Changes

Summary

merged
more NEWS;
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
more informative error message, e.g. relevant for incoherent imports;
syntax for pattern aliases

Changeset 66455:158c513a39f5 by wenzelm: merged
Changeset 66454:1a73ad1c06dd by wenzelm: more NEWS;
The file was modified	`NEWS` (diff)
Changeset 66453:cc19f7ca2ed6 by wenzelm: session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
The file was modified	`src/Benchmarks/Datatype_Benchmark/IsaFoR.thy` (diff)
The file was modified	`src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy` (diff)
The file was modified	`src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy` (diff)
The file was modified	`src/CCL/Set.thy` (diff)
The file was modified	`src/Doc/Codegen/Adaptation.thy` (diff)
The file was modified	`src/Doc/Codegen/Computations.thy` (diff)
The file was modified	`src/Doc/Codegen/Evaluation.thy` (diff)
The file was modified	`src/Doc/Codegen/Further.thy` (diff)
The file was modified	`src/Doc/Codegen/Inductive_Predicate.thy` (diff)
The file was modified	`src/Doc/Codegen/Introduction.thy` (diff)
The file was modified	`src/Doc/Codegen/Refinement.thy` (diff)
The file was modified	`src/Doc/Codegen/Setup.thy` (diff)
The file was modified	`src/Doc/Corec/Corec.thy` (diff)
The file was modified	`src/Doc/Datatypes/Datatypes.thy` (diff)
The file was modified	`src/Doc/Eisbach/Manual.thy` (diff)
The file was modified	`src/Doc/Eisbach/Preface.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/HOL_Specific.thy` (diff)
The file was modified	`src/Doc/Logics_ZF/FOL_examples.thy` (diff)
The file was modified	`src/Doc/Logics_ZF/IFOL_examples.thy` (diff)
The file was modified	`src/Doc/Logics_ZF/If.thy` (diff)
The file was modified	`src/Doc/ROOT` (diff)
The file was modified	`src/Doc/Sugar/Sugar.thy` (diff)
The file was modified	`src/Doc/Typeclass_Hierarchy/Setup.thy` (diff)
The file was modified	`src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy` (diff)
The file was modified	`src/HOL/Algebra/Congruence.thy` (diff)
The file was modified	`src/HOL/Algebra/Divisibility.thy` (diff)
The file was modified	`src/HOL/Algebra/Exponent.thy` (diff)
The file was modified	`src/HOL/Algebra/Group.thy` (diff)
The file was modified	`src/HOL/Algebra/IntRing.thy` (diff)
The file was modified	`src/HOL/Algebra/Order.thy` (diff)
The file was modified	`src/HOL/Analysis/Arcwise_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Analysis_Basics.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Analysis/Continuum_Not_Denumerable.thy` (diff)
The file was modified	`src/HOL/Analysis/Convex_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Determinants.thy` (diff)
The file was modified	`src/HOL/Analysis/Extended_Real_Limits.thy` (diff)
The file was modified	`src/HOL/Analysis/Finite_Cartesian_Product.thy` (diff)
The file was modified	`src/HOL/Analysis/Gamma_Function.thy` (diff)
The file was modified	`src/HOL/Analysis/L2_Norm.thy` (diff)
The file was modified	`src/HOL/Analysis/Linear_Algebra.thy` (diff)
The file was modified	`src/HOL/Analysis/Measurable.thy` (diff)
The file was modified	`src/HOL/Analysis/Measure_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Norm_Arith.thy` (diff)
The file was modified	`src/HOL/Analysis/Ordered_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Product_Vector.thy` (diff)
The file was modified	`src/HOL/Analysis/Sigma_Algebra.thy` (diff)
The file was modified	`src/HOL/Analysis/Summation_Tests.thy` (diff)
The file was modified	`src/HOL/Analysis/Topology_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/ex/Approximations.thy` (diff)
The file was modified	`src/HOL/Analysis/ex/Circle_Area.thy` (diff)
The file was modified	`src/HOL/Auth/Smartcard/EventSC.thy` (diff)
The file was modified	`src/HOL/Auth/TLS.thy` (diff)
The file was modified	`src/HOL/Bali/Basis.thy` (diff)
The file was modified	`src/HOL/Cardinals/Cardinal_Arithmetic.thy` (diff)
The file was modified	`src/HOL/Cardinals/Cardinal_Order_Relation.thy` (diff)
The file was modified	`src/HOL/Cardinals/Order_Union.thy` (diff)
The file was modified	`src/HOL/Cardinals/Wellfounded_More.thy` (diff)
The file was modified	`src/HOL/Cardinals/Wellorder_Constructions.thy` (diff)
The file was modified	`src/HOL/Cardinals/Wellorder_Embedding.thy` (diff)
The file was modified	`src/HOL/Cardinals/Wellorder_Relation.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Candidates.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Code_Test_GHC.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Code_Test_MLton.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Code_Test_OCaml.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Code_Test_PolyML.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Code_Test_Scala.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Generate.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Generate_Target_Nat.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Factorial_Ring.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Polynomial.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Primes.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/LFilter.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Paper_Examples.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Stream_Processor.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Tests/Iterate_GPV.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Tests/Merge_A.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Tests/Merge_Poly.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Tests/Misc_Mono.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Tests/Misc_Poly.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Tests/Simple_Nesting.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Tests/Small_Concrete.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Tests/Stream_Friends.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Tests/TLList_Friends.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Tests/Type_Class.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AVL_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Balance.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Brother12_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Priority_Queue.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Splay_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree_Set.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Compat.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Koenig.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Lambda_Term.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Misc_Codatatype.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Misc_Datatype.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Process.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Stream_Processor.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/TreeFsetI.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Algebra_Aux.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Approximation.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Approximation_Bounds.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Commutative_Ring.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Cooper.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Ferrack.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/MIR.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy` (diff)
The file was modified	`src/HOL/Eisbach/Examples_FOL.thy` (diff)
The file was modified	`src/HOL/HOLCF/Bifinite.thy` (diff)
The file was modified	`src/HOL/HOLCF/FOCUS/Fstream.thy` (diff)
The file was modified	`src/HOL/HOLCF/FOCUS/Fstreams.thy` (diff)
The file was modified	`src/HOL/HOLCF/FOCUS/Stream_adm.thy` (diff)
The file was modified	`src/HOL/HOLCF/IMP/Denotational.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/ABP/Abschannel.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/ABP/Correctness.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/ABP/Env.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/ABP/Receiver.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/ABP/Sender.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/ABP/Spec.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Abschannel.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Receiver.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Sender.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Spec.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/Seq.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/Storage/Correctness.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/Storage/Impl.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/Storage/Spec.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/ex/TrivEx.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/ex/TrivEx2.thy` (diff)
The file was modified	`src/HOL/HOLCF/Library/Defl_Bifinite.thy` (diff)
The file was modified	`src/HOL/HOLCF/Library/Stream.thy` (diff)
The file was modified	`src/HOL/HOLCF/Representable.thy` (diff)
The file was modified	`src/HOL/HOLCF/Universal.thy` (diff)
The file was modified	`src/HOL/HOLCF/ex/Dagstuhl.thy` (diff)
The file was modified	`src/HOL/HOLCF/ex/Focus_ex.thy` (diff)
The file was modified	`src/HOL/Hahn_Banach/Bounds.thy` (diff)
The file was modified	`src/HOL/Hahn_Banach/Subspace.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int_init.thy` (diff)
The file was modified	`src/HOL/IMP/Live_True.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/Heap.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/Heap_Monad.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/Overview.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/ex/Linked_Lists.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/ex/List_Sublist.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/ex/SatChecker.thy` (diff)
The file was modified	`src/HOL/Induct/Sexp.thy` (diff)
The file was modified	`src/HOL/Isar_Examples/Fibonacci.thy` (diff)
The file was modified	`src/HOL/Isar_Examples/Knaster_Tarski.thy` (diff)
The file was modified	`src/HOL/Library/Countable.thy` (diff)
The file was modified	`src/HOL/Library/Countable_Set_Type.thy` (diff)
The file was modified	`src/HOL/Library/FuncSet.thy` (diff)
The file was modified	`src/HOL/Library/Lattice_Syntax.thy` (diff)
The file was modified	`src/HOL/Library/ListVector.thy` (diff)
The file was modified	`src/HOL/Library/Option_ord.thy` (diff)
The file was modified	`src/HOL/Library/Preorder.thy` (diff)
The file was modified	`src/HOL/Matrix_LP/ComputeFloat.thy` (diff)
The file was modified	`src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy` (diff)
The file was modified	`src/HOL/Matrix_LP/LP.thy` (diff)
The file was modified	`src/HOL/Matrix_LP/Matrix.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Abstraction.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Big_O.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Tarski.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/Kildall.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/Semilat.thy` (diff)
The file was modified	`src/HOL/MicroJava/J/JBasis.thy` (diff)
The file was modified	`src/HOL/Mutabelle/MutabelleExtra.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Manual_Nits.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/CK_Machine.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/CR_Takahashi.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Class1.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Compile.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Contexts.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Crary.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Fsub.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Height.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Lam_Funs.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Lambda_mu.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/LocalWeakening.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Pattern.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/SOS.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Standardization.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Support.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Type_Preservation.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/VC_Condition.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/W.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Weakening.thy` (diff)
The file was modified	`src/HOL/Nominal/Nominal.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HSEQ.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HTranscendental.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/NSA.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Cong.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Eratosthenes.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Prime_Powers.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Residues.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Totient.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/Examples.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/IMP_1.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/IMP_2.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/IMP_3.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/IMP_4.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/Lambda_Example.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/List_Examples.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy` (diff)
The file was modified	`src/HOL/Probability/Discrete_Topology.thy` (diff)
The file was modified	`src/HOL/Probability/Essential_Supremum.thy` (diff)
The file was modified	`src/HOL/Probability/Fin_Map.thy` (diff)
The file was modified	`src/HOL/Probability/Giry_Monad.thy` (diff)
The file was modified	`src/HOL/Probability/Helly_Selection.thy` (diff)
The file was modified	`src/HOL/Probability/PMF_Impl.thy` (diff)
The file was modified	`src/HOL/Probability/Probability_Mass_Function.thy` (diff)
The file was modified	`src/HOL/Probability/Probability_Measure.thy` (diff)
The file was modified	`src/HOL/Probability/Projective_Limit.thy` (diff)
The file was modified	`src/HOL/Probability/Random_Permutations.thy` (diff)
The file was modified	`src/HOL/Probability/SPMF.thy` (diff)
The file was modified	`src/HOL/Probability/Stopping_Time.thy` (diff)
The file was modified	`src/HOL/Probability/Stream_Space.thy` (diff)
The file was modified	`src/HOL/Probability/Tree_Space.thy` (diff)
The file was modified	`src/HOL/Probability/ex/Dining_Cryptographers.thy` (diff)
The file was modified	`src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy` (diff)
The file was modified	`src/HOL/Probability/ex/Measure_Not_CCC.thy` (diff)
The file was modified	`src/HOL/Prolog/HOHH.thy` (diff)
The file was modified	`src/HOL/Proofs/Extraction/Euclid.thy` (diff)
The file was modified	`src/HOL/Proofs/Extraction/Higman_Extraction.thy` (diff)
The file was modified	`src/HOL/Proofs/Extraction/Pigeonhole.thy` (diff)
The file was modified	`src/HOL/Proofs/Extraction/QuotRem.thy` (diff)
The file was modified	`src/HOL/Proofs/Extraction/Warshall.thy` (diff)
The file was modified	`src/HOL/Proofs/ex/XML_Data.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Examples/Hotel_Example.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/DList.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/Int_Pow.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/Lift_Fun.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/Quotient_FSet.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/Quotient_Int.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/Quotient_Message.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/Quotient_Rat.thy` (diff)
The file was modified	`src/HOL/ROOT` (diff)
The file was modified	`src/HOL/SET_Protocol/Message_SET.thy` (diff)
The file was modified	`src/HOL/SMT_Examples/SMT_Word_Examples.thy` (diff)
The file was modified	`src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy` (diff)
The file was modified	`src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy` (diff)
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy` (diff)
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy` (diff)
The file was modified	`src/HOL/SPARK/Examples/Sqrt/Sqrt.thy` (diff)
The file was modified	`src/HOL/SPARK/Manual/Complex_Types.thy` (diff)
The file was modified	`src/HOL/SPARK/Manual/Example_Verification.thy` (diff)
The file was modified	`src/HOL/SPARK/Manual/Proc1.thy` (diff)
The file was modified	`src/HOL/SPARK/Manual/Proc2.thy` (diff)
The file was modified	`src/HOL/SPARK/Manual/Reference.thy` (diff)
The file was modified	`src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy` (diff)
The file was modified	`src/HOL/SPARK/SPARK_Setup.thy` (diff)
The file was modified	`src/HOL/TLA/Buffer/Buffer.thy` (diff)
The file was modified	`src/HOL/TLA/Inc/Inc.thy` (diff)
The file was modified	`src/HOL/TLA/Memory/ProcedureInterface.thy` (diff)
The file was modified	`src/HOL/TPTP/ATP_Problem_Import.thy` (diff)
The file was modified	`src/HOL/UNITY/Comp/AllocBase.thy` (diff)
The file was modified	`src/HOL/UNITY/Follows.thy` (diff)
The file was modified	`src/HOL/UNITY/Simple/NSP_Bad.thy` (diff)
The file was modified	`src/HOL/Unix/Unix.thy` (diff)
The file was modified	`src/HOL/Word/Bits_Bit.thy` (diff)
The file was modified	`src/HOL/Word/Examples/WordExamples.thy` (diff)
The file was modified	`src/HOL/Word/Word.thy` (diff)
The file was modified	`src/HOL/Word/Word_Miscellaneous.thy` (diff)
The file was modified	`src/HOL/ZF/LProd.thy` (diff)
The file was modified	`src/HOL/ex/Adhoc_Overloading_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Ballot.thy` (diff)
The file was modified	`src/HOL/ex/Birthday_Paradox.thy` (diff)
The file was modified	`src/HOL/ex/Bubblesort.thy` (diff)
The file was modified	`src/HOL/ex/Code_Binary_Nat_examples.thy` (diff)
The file was modified	`src/HOL/ex/Code_Timing.thy` (diff)
The file was modified	`src/HOL/ex/Computations.thy` (diff)
The file was modified	`src/HOL/ex/Execute_Choice.thy` (diff)
The file was modified	`src/HOL/ex/Functions.thy` (diff)
The file was modified	`src/HOL/ex/Groebner_Examples.thy` (diff)
The file was modified	`src/HOL/ex/IArray_Examples.thy` (diff)
The file was modified	`src/HOL/ex/MergeSort.thy` (diff)
The file was modified	`src/HOL/ex/Parallel_Example.thy` (diff)
The file was modified	`src/HOL/ex/Perm_Fragments.thy` (diff)
The file was modified	`src/HOL/ex/PresburgerEx.thy` (diff)
The file was modified	`src/HOL/ex/Quicksort.thy` (diff)
The file was modified	`src/HOL/ex/Reflection_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Refute_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Rewrite_Examples.thy` (diff)
The file was modified	`src/HOL/ex/SOS.thy` (diff)
The file was modified	`src/HOL/ex/SOS_Cert.thy` (diff)
The file was modified	`src/HOL/ex/Simps_Case_Conv_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Sqrt.thy` (diff)
The file was modified	`src/HOL/ex/Sqrt_Script.thy` (diff)
The file was modified	`src/HOL/ex/Tarski.thy` (diff)
The file was modified	`src/HOL/ex/Termination.thy` (diff)
The file was modified	`src/HOL/ex/ThreeDivides.thy` (diff)
The file was modified	`src/HOL/ex/Transfer_Debug.thy` (diff)
The file was modified	`src/HOL/ex/Transitive_Closure_Table_Ex.thy` (diff)
The file was modified	`src/HOL/ex/While_Combinator_Example.thy` (diff)
The file was modified	`src/HOL/ex/Word_Type.thy` (diff)
The file was modified	`src/LCF/LCF.thy` (diff)
The file was modified	`src/ZF/UNITY/MultisetSum.thy` (diff)
The file was modified	`src/ZF/ZF_Base.thy` (diff)
Changeset 66452:450cefec7c11 by wenzelm: more informative error message, e.g. relevant for incoherent imports;
The file was modified	`src/Pure/context.ML` (diff)
Changeset 66451:5be0b0604d71 by lars hupel _lars.hupel@mytum.de_: syntax for pattern aliases
The file was added	`src/HOL/Library/Pattern_Aliases.thy`
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Library/Library.thy` (diff)