Changes

Summary

documentation on "isabelle update";
eliminated spurious \<^print>;
isabelle update -u control_cartouches;
latex macro for \<^const>;
mark for isabelle update -u control_cartouches;
proper session base foundations (amending e848328cb2c1);

Changeset 69599:caa7e406056d by wenzelm: documentation on "isabelle update";
The file was modified	`src/Doc/Isar_Ref/document/style.sty` (diff)
The file was modified	`src/Doc/System/Sessions.thy` (diff)
Changeset 69598:81caae4fc4fa by wenzelm: eliminated spurious \<^print>;
The file was modified	`src/HOL/Library/datatype_records.ML` (diff)
Changeset 69597:ff784d5a5bfb by wenzelm: isabelle update -u control_cartouches;
The file was modified	`src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy` (diff)
The file was modified	`src/Benchmarks/Record_Benchmark/Record_Benchmark.thy` (diff)
The file was modified	`src/Doc/Classes/Classes.thy` (diff)
The file was modified	`src/Doc/Classes/Setup.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/Foundations.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/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/Functions/Functions.thy` (diff)
The file was modified	`src/Doc/How_to_Prove_it/How_to_Prove_it.thy` (diff)
The file was modified	`src/Doc/Implementation/Eq.thy` (diff)
The file was modified	`src/Doc/Implementation/Integration.thy` (diff)
The file was modified	`src/Doc/Implementation/Isar.thy` (diff)
The file was modified	`src/Doc/Implementation/Local_Theory.thy` (diff)
The file was modified	`src/Doc/Implementation/Logic.thy` (diff)
The file was modified	`src/Doc/Implementation/ML.thy` (diff)
The file was modified	`src/Doc/Implementation/Prelim.thy` (diff)
The file was modified	`src/Doc/Implementation/Proof.thy` (diff)
The file was modified	`src/Doc/Implementation/Syntax.thy` (diff)
The file was modified	`src/Doc/Implementation/Tactic.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Document_Preparation.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Framework.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Generic.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/HOL_Specific.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Inner_Syntax.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Outer_Syntax.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Proof.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Proof_Script.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Spec.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Synopsis.thy` (diff)
The file was modified	`src/Doc/JEdit/JEdit.thy` (diff)
The file was modified	`src/Doc/Locales/Examples.thy` (diff)
The file was modified	`src/Doc/Locales/Examples1.thy` (diff)
The file was modified	`src/Doc/Locales/Examples2.thy` (diff)
The file was modified	`src/Doc/Locales/Examples3.thy` (diff)
The file was modified	`src/Doc/Main/Main_Doc.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/Basics.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/Bool_nat_list.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/Isar.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/Logic.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/Types_and_funs.thy` (diff)
The file was modified	`src/Doc/Sugar/Sugar.thy` (diff)
The file was modified	`src/Doc/Tutorial/Advanced/simp2.thy` (diff)
The file was modified	`src/Doc/Tutorial/CTL/Base.thy` (diff)
The file was modified	`src/Doc/Tutorial/CTL/CTL.thy` (diff)
The file was modified	`src/Doc/Tutorial/CTL/CTLind.thy` (diff)
The file was modified	`src/Doc/Tutorial/CTL/PDL.thy` (diff)
The file was modified	`src/Doc/Tutorial/CodeGen/CodeGen.thy` (diff)
The file was modified	`src/Doc/Tutorial/Datatype/ABexpr.thy` (diff)
The file was modified	`src/Doc/Tutorial/Datatype/Fundata.thy` (diff)
The file was modified	`src/Doc/Tutorial/Datatype/Nested.thy` (diff)
The file was modified	`src/Doc/Tutorial/Documents/Documents.thy` (diff)
The file was modified	`src/Doc/Tutorial/Fun/fun0.thy` (diff)
The file was modified	`src/Doc/Tutorial/Ifexpr/Ifexpr.thy` (diff)
The file was modified	`src/Doc/Tutorial/Inductive/AB.thy` (diff)
The file was modified	`src/Doc/Tutorial/Inductive/Advanced.thy` (diff)
The file was modified	`src/Doc/Tutorial/Inductive/Even.thy` (diff)
The file was modified	`src/Doc/Tutorial/Inductive/Mutual.thy` (diff)
The file was modified	`src/Doc/Tutorial/Inductive/Star.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/AdvancedInd.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/Itrev.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/Option2.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/Tree.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/Tree2.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/case_exprs.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/natsum.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/pairs2.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/prime_def.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/simp.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/types.thy` (diff)
The file was modified	`src/Doc/Tutorial/Protocol/Event.thy` (diff)
The file was modified	`src/Doc/Tutorial/Protocol/Message.thy` (diff)
The file was modified	`src/Doc/Tutorial/Protocol/NS_Public.thy` (diff)
The file was modified	`src/Doc/Tutorial/Rules/Basic.thy` (diff)
The file was modified	`src/Doc/Tutorial/Sets/Recur.thy` (diff)
The file was modified	`src/Doc/Tutorial/ToyList/ToyList.thy` (diff)
The file was modified	`src/Doc/Tutorial/ToyList/ToyList_Test.thy` (diff)
The file was modified	`src/Doc/Tutorial/Trie/Trie.thy` (diff)
The file was modified	`src/Doc/Tutorial/Types/Axioms.thy` (diff)
The file was modified	`src/Doc/Tutorial/Types/Numbers.thy` (diff)
The file was modified	`src/Doc/Tutorial/Types/Overloading.thy` (diff)
The file was modified	`src/Doc/Tutorial/Types/Pairs.thy` (diff)
The file was modified	`src/Doc/Tutorial/Types/Records.thy` (diff)
The file was modified	`src/Doc/Tutorial/Types/Typedefs.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/Doc/more_antiquote.ML` (diff)
The file was modified	`src/FOL/FOL.thy` (diff)
The file was modified	`src/HOL/Algebra/AbelCoset.thy` (diff)
The file was modified	`src/HOL/Algebra/Complete_Lattice.thy` (diff)
The file was modified	`src/HOL/Algebra/Coset.thy` (diff)
The file was modified	`src/HOL/Algebra/Divisibility.thy` (diff)
The file was modified	`src/HOL/Algebra/Embedded_Algebras.thy` (diff)
The file was modified	`src/HOL/Algebra/Group.thy` (diff)
The file was modified	`src/HOL/Algebra/Ideal.thy` (diff)
The file was modified	`src/HOL/Algebra/IntRing.thy` (diff)
The file was modified	`src/HOL/Algebra/Multiplicative_Group.thy` (diff)
The file was modified	`src/HOL/Algebra/Order.thy` (diff)
The file was modified	`src/HOL/Algebra/QuotRing.thy` (diff)
The file was modified	`src/HOL/Algebra/Ring_Divisibility.thy` (diff)
The file was modified	`src/HOL/Algebra/Sylow.thy` (diff)
The file was modified	`src/HOL/Algebra/Sym_Groups.thy` (diff)
The file was modified	`src/HOL/Algebra/UnivPoly.thy` (diff)
The file was modified	`src/HOL/Analysis/Bochner_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Borel_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Bounded_Linear_Function.thy` (diff)
The file was modified	`src/HOL/Analysis/Cartesian_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Cauchy_Integral_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Analysis/Conformal_Mappings.thy` (diff)
The file was modified	`src/HOL/Analysis/Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Continuum_Not_Denumerable.thy` (diff)
The file was modified	`src/HOL/Analysis/Derivative.thy` (diff)
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/FPS_Convergence.thy` (diff)
The file was modified	`src/HOL/Analysis/Finite_Cartesian_Product.thy` (diff)
The file was modified	`src/HOL/Analysis/Finite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Function_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Gamma_Function.thy` (diff)
The file was modified	`src/HOL/Analysis/Harmonic_Numbers.thy` (diff)
The file was modified	`src/HOL/Analysis/Henstock_Kurzweil_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Infinite_Set_Sum.thy` (diff)
The file was modified	`src/HOL/Analysis/Inner_Product.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/Polytope.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/Tagged_Division.thy` (diff)
The file was modified	`src/HOL/Analysis/Uniform_Limit.thy` (diff)
The file was modified	`src/HOL/Analysis/Weierstrass_Theorems.thy` (diff)
The file was modified	`src/HOL/Analysis/ex/Approximations.thy` (diff)
The file was modified	`src/HOL/Analysis/measurable.ML` (diff)
The file was modified	`src/HOL/Analysis/normarith.ML` (diff)
The file was modified	`src/HOL/Auth/CertifiedEmail.thy` (diff)
The file was modified	`src/HOL/Auth/Event.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Analz.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Extensions.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Guard.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/GuardK.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Guard_Public.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Guard_Shared.thy` (diff)
The file was modified	`src/HOL/Auth/KerberosIV.thy` (diff)
The file was modified	`src/HOL/Auth/KerberosIV_Gets.thy` (diff)
The file was modified	`src/HOL/Auth/KerberosV.thy` (diff)
The file was modified	`src/HOL/Auth/Message.thy` (diff)
The file was modified	`src/HOL/Auth/NS_Shared.thy` (diff)
The file was modified	`src/HOL/Auth/OtwayRees.thy` (diff)
The file was modified	`src/HOL/Auth/OtwayReesBella.thy` (diff)
The file was modified	`src/HOL/Auth/OtwayRees_AN.thy` (diff)
The file was modified	`src/HOL/Auth/OtwayRees_Bad.thy` (diff)
The file was modified	`src/HOL/Auth/Public.thy` (diff)
The file was modified	`src/HOL/Auth/Recur.thy` (diff)
The file was modified	`src/HOL/Auth/Shared.thy` (diff)
The file was modified	`src/HOL/Auth/Smartcard/EventSC.thy` (diff)
The file was modified	`src/HOL/Auth/Smartcard/ShoupRubin.thy` (diff)
The file was modified	`src/HOL/Auth/Smartcard/ShoupRubinBella.thy` (diff)
The file was modified	`src/HOL/Auth/Smartcard/Smartcard.thy` (diff)
The file was modified	`src/HOL/Auth/TLS.thy` (diff)
The file was modified	`src/HOL/Auth/Yahalom.thy` (diff)
The file was modified	`src/HOL/Auth/Yahalom2.thy` (diff)
The file was modified	`src/HOL/Auth/Yahalom_Bad.thy` (diff)
The file was modified	`src/HOL/Auth/ZhouGollmann.thy` (diff)
The file was modified	`src/HOL/Bali/AxCompl.thy` (diff)
The file was modified	`src/HOL/Bali/AxExample.thy` (diff)
The file was modified	`src/HOL/Bali/AxSem.thy` (diff)
The file was modified	`src/HOL/Bali/AxSound.thy` (diff)
The file was modified	`src/HOL/Bali/DeclConcepts.thy` (diff)
The file was modified	`src/HOL/Bali/DefiniteAssignment.thy` (diff)
The file was modified	`src/HOL/Bali/DefiniteAssignmentCorrect.thy` (diff)
The file was modified	`src/HOL/Bali/Eval.thy` (diff)
The file was modified	`src/HOL/Bali/Evaln.thy` (diff)
The file was modified	`src/HOL/Bali/Example.thy` (diff)
The file was modified	`src/HOL/Bali/Table.thy` (diff)
The file was modified	`src/HOL/Bali/Term.thy` (diff)
The file was modified	`src/HOL/Bali/TypeSafe.thy` (diff)
The file was modified	`src/HOL/Bali/WellForm.thy` (diff)
The file was modified	`src/HOL/Bali/WellType.thy` (diff)
The file was modified	`src/HOL/Cardinals/Wellorder_Extension.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Candidates.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Code_Lazy_Test.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_OCaml.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Code_Test_Scala.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Formal_Power_Series.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Polynomial.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Polynomial_FPS.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Primes.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AA_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AList_Upd_Del.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AVL_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Array_Braun.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Binomial_Heap.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Less_False.thy` (diff)
The file was modified	`src/HOL/Data_Structures/List_Ins_Del.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Set2_Join.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Set2_Join_RBT.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Sorted_Less.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Sorting.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree234_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree23_Set.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Compat.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Stream_Processor.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/Conversions.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Cooper.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Dense_Linear_Order.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/Decision_Procs/Polynomial_List.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Rat_Pair.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Reflective_Field.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/approximation.ML` (diff)
The file was modified	`src/HOL/Decision_Procs/approximation_generator.ML` (diff)
The file was modified	`src/HOL/Decision_Procs/cooper_tac.ML` (diff)
The file was modified	`src/HOL/Decision_Procs/ex/Approximation_Ex.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/ferrack_tac.ML` (diff)
The file was modified	`src/HOL/Decision_Procs/ferrante_rackoff.ML` (diff)
The file was modified	`src/HOL/Decision_Procs/ferrante_rackoff_data.ML` (diff)
The file was modified	`src/HOL/Decision_Procs/langford.ML` (diff)
The file was modified	`src/HOL/Decision_Procs/langford_data.ML` (diff)
The file was modified	`src/HOL/Decision_Procs/mir_tac.ML` (diff)
The file was modified	`src/HOL/Eisbach/Examples.thy` (diff)
The file was modified	`src/HOL/Eisbach/Tests.thy` (diff)
The file was modified	`src/HOL/HOL.thy` (diff)
The file was modified	`src/HOL/HOLCF/Bifinite.thy` (diff)
The file was modified	`src/HOL/HOLCF/Cfun.thy` (diff)
The file was modified	`src/HOL/HOLCF/Cpodef.thy` (diff)
The file was modified	`src/HOL/HOLCF/Domain.thy` (diff)
The file was modified	`src/HOL/HOLCF/FOCUS/Buffer_adm.thy` (diff)
The file was modified	`src/HOL/HOLCF/FOCUS/Fstream.thy` (diff)
The file was modified	`src/HOL/HOLCF/Fix.thy` (diff)
The file was modified	`src/HOL/HOLCF/Fixrec.thy` (diff)
The file was modified	`src/HOL/HOLCF/Fun_Cpo.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/ABP/Correctness.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/Automata.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/CompoScheds.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/CompoTraces.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Impl.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/ShortExecutions.thy` (diff)
The file was modified	`src/HOL/HOLCF/Library/Bool_Discrete.thy` (diff)
The file was modified	`src/HOL/HOLCF/Library/Char_Discrete.thy` (diff)
The file was modified	`src/HOL/HOLCF/Library/Int_Discrete.thy` (diff)
The file was modified	`src/HOL/HOLCF/Library/List_Cpo.thy` (diff)
The file was modified	`src/HOL/HOLCF/Library/List_Predomain.thy` (diff)
The file was modified	`src/HOL/HOLCF/Library/Nat_Discrete.thy` (diff)
The file was modified	`src/HOL/HOLCF/Library/Option_Cpo.thy` (diff)
The file was modified	`src/HOL/HOLCF/Library/Sum_Cpo.thy` (diff)
The file was modified	`src/HOL/HOLCF/Lift.thy` (diff)
The file was modified	`src/HOL/HOLCF/One.thy` (diff)
The file was modified	`src/HOL/HOLCF/Pcpo.thy` (diff)
The file was modified	`src/HOL/HOLCF/Porder.thy` (diff)
The file was modified	`src/HOL/HOLCF/Powerdomains.thy` (diff)
The file was modified	`src/HOL/HOLCF/Product_Cpo.thy` (diff)
The file was modified	`src/HOL/HOLCF/Representable.thy` (diff)
The file was modified	`src/HOL/HOLCF/Tools/Domain/domain.ML` (diff)
The file was modified	`src/HOL/HOLCF/Tools/Domain/domain_axioms.ML` (diff)
The file was modified	`src/HOL/HOLCF/Tools/Domain/domain_constructors.ML` (diff)
The file was modified	`src/HOL/HOLCF/Tools/Domain/domain_induction.ML` (diff)
The file was modified	`src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML` (diff)
The file was modified	`src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML` (diff)
The file was modified	`src/HOL/HOLCF/Tools/cont_consts.ML` (diff)
The file was modified	`src/HOL/HOLCF/Tools/cont_proc.ML` (diff)
The file was modified	`src/HOL/HOLCF/Tools/cpodef.ML` (diff)
The file was modified	`src/HOL/HOLCF/Tools/domaindef.ML` (diff)
The file was modified	`src/HOL/HOLCF/Tools/fixrec.ML` (diff)
The file was modified	`src/HOL/HOLCF/Tools/holcf_library.ML` (diff)
The file was modified	`src/HOL/HOLCF/Tr.thy` (diff)
The file was modified	`src/HOL/HOLCF/Tutorial/Fixrec_ex.thy` (diff)
The file was modified	`src/HOL/HOLCF/Up.thy` (diff)
The file was modified	`src/HOL/HOLCF/ex/Focus_ex.thy` (diff)
The file was modified	`src/HOL/HOLCF/ex/Pattern_Match.thy` (diff)
The file was modified	`src/HOL/Hahn_Banach/Vector_Space.thy` (diff)
The file was modified	`src/HOL/Hoare/Heap.thy` (diff)
The file was modified	`src/HOL/Hoare/HeapSyntaxAbort.thy` (diff)
The file was modified	`src/HOL/Hoare/Hoare_Logic.thy` (diff)
The file was modified	`src/HOL/Hoare/Hoare_Logic_Abort.thy` (diff)
The file was modified	`src/HOL/Hoare/Pointer_Examples.thy` (diff)
The file was modified	`src/HOL/Hoare/Pointers0.thy` (diff)
The file was modified	`src/HOL/Hoare/SchorrWaite.thy` (diff)
The file was modified	`src/HOL/Hoare/Separation.thy` (diff)
The file was modified	`src/HOL/Hoare/hoare_syntax.ML` (diff)
The file was modified	`src/HOL/Hoare/hoare_tac.ML` (diff)
The file was modified	`src/HOL/Hoare_Parallel/Gar_Coll.thy` (diff)
The file was modified	`src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy` (diff)
The file was modified	`src/HOL/Hoare_Parallel/OG_Examples.thy` (diff)
The file was modified	`src/HOL/Hoare_Parallel/OG_Syntax.thy` (diff)
The file was modified	`src/HOL/Hoare_Parallel/Quote_Antiquote.thy` (diff)
The file was modified	`src/HOL/Hoare_Parallel/RG_Syntax.thy` (diff)
The file was modified	`src/HOL/IMP/AExp.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int0.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int1_parity.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int2.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int3.thy` (diff)
The file was modified	`src/HOL/IMP/Big_Step.thy` (diff)
The file was modified	`src/HOL/IMP/C_like.thy` (diff)
The file was modified	`src/HOL/IMP/Collecting1.thy` (diff)
The file was modified	`src/HOL/IMP/Compiler.thy` (diff)
The file was modified	`src/HOL/IMP/Compiler2.thy` (diff)
The file was modified	`src/HOL/IMP/Def_Init_Big.thy` (diff)
The file was modified	`src/HOL/IMP/Hoare_Total.thy` (diff)
The file was modified	`src/HOL/IMP/Live_True.thy` (diff)
The file was modified	`src/HOL/IMP/Sec_Typing.thy` (diff)
The file was modified	`src/HOL/IMP/Sec_TypingT.thy` (diff)
The file was modified	`src/HOL/IMP/Types.thy` (diff)
The file was modified	`src/HOL/IMP/Vars.thy` (diff)
The file was modified	`src/HOL/IMPP/Hoare.thy` (diff)
The file was modified	`src/HOL/IMPP/Misc.thy` (diff)
The file was modified	`src/HOL/IMPP/Natural.thy` (diff)
The file was modified	`src/HOL/IOA/Solve.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/Linked_Lists.thy` (diff)
The file was modified	`src/HOL/Import/import_data.ML` (diff)
The file was modified	`src/HOL/Import/import_rule.ML` (diff)
The file was modified	`src/HOL/Induct/Comb.thy` (diff)
The file was modified	`src/HOL/Induct/PropLog.thy` (diff)
The file was modified	`src/HOL/Induct/QuoDataType.thy` (diff)
The file was modified	`src/HOL/Induct/QuoNestedDataType.thy` (diff)
The file was modified	`src/HOL/Isar_Examples/Cantor.thy` (diff)
The file was modified	`src/HOL/Isar_Examples/Hoare.thy` (diff)
The file was modified	`src/HOL/Isar_Examples/Structured_Statements.thy` (diff)
The file was modified	`src/HOL/Lattice/Lattice.thy` (diff)
The file was modified	`src/HOL/Lattice/Orders.thy` (diff)
The file was modified	`src/HOL/Library/Going_To_Filter.thy` (diff)
The file was modified	`src/HOL/Library/Landau_Symbols.thy` (diff)
The file was modified	`src/HOL/Library/Lub_Glb.thy` (diff)
The file was modified	`src/HOL/Library/Omega_Words_Fun.thy` (diff)
The file was modified	`src/HOL/Library/Pattern_Aliases.thy` (diff)
The file was modified	`src/HOL/Library/Permutation.thy` (diff)
The file was modified	`src/HOL/Library/Stream.thy` (diff)
The file was modified	`src/HOL/Library/Type_Length.thy` (diff)
The file was modified	`src/HOL/Library/code_lazy.ML` (diff)
The file was modified	`src/HOL/Library/code_test.ML` (diff)
The file was modified	`src/HOL/Matrix_LP/Compute_Oracle/compute.ML` (diff)
The file was modified	`src/HOL/Matrix_LP/float_arith.ML` (diff)
The file was modified	`src/HOL/Matrix_LP/fspmlp.ML` (diff)
The file was modified	`src/HOL/Matrix_LP/matrixlp.ML` (diff)
The file was modified	`src/HOL/Metis_Examples/Message.thy` (diff)
The file was modified	`src/HOL/MicroJava/BV/BVExample.thy` (diff)
The file was modified	`src/HOL/MicroJava/BV/BVSpec.thy` (diff)
The file was modified	`src/HOL/MicroJava/BV/Effect.thy` (diff)
The file was modified	`src/HOL/MicroJava/BV/Typing_Framework_JVM.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/Err.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/Typing_Framework_err.thy` (diff)
The file was modified	`src/HOL/MicroJava/J/JTypeSafe.thy` (diff)
The file was modified	`src/HOL/MicroJava/J/State.thy` (diff)
The file was modified	`src/HOL/MicroJava/J/WellForm.thy` (diff)
The file was modified	`src/HOL/MicroJava/JVM/JVMExceptions.thy` (diff)
The file was modified	`src/HOL/MicroJava/JVM/JVMListExample.thy` (diff)
The file was modified	`src/HOL/Mirabelle/Tools/mirabelle.ML` (diff)
The file was modified	`src/HOL/Mutabelle/MutabelleExtra.thy` (diff)
The file was modified	`src/HOL/Mutabelle/mutabelle.ML` (diff)
The file was modified	`src/HOL/Mutabelle/mutabelle_extra.ML` (diff)
The file was modified	`src/HOL/NanoJava/AxSem.thy` (diff)
The file was modified	`src/HOL/NanoJava/Equivalence.thy` (diff)
The file was modified	`src/HOL/NanoJava/Example.thy` (diff)
The file was modified	`src/HOL/NanoJava/State.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Manual_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Mini_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Mono_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Refute_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/minipick.ML` (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/Standardization.thy` (diff)
The file was modified	`src/HOL/Nominal/Nominal.thy` (diff)
The file was modified	`src/HOL/Nominal/nominal_atoms.ML` (diff)
The file was modified	`src/HOL/Nominal/nominal_datatype.ML` (diff)
The file was modified	`src/HOL/Nominal/nominal_fresh_fun.ML` (diff)
The file was modified	`src/HOL/Nominal/nominal_inductive.ML` (diff)
The file was modified	`src/HOL/Nominal/nominal_inductive2.ML` (diff)
The file was modified	`src/HOL/Nominal/nominal_permeq.ML` (diff)
The file was modified	`src/HOL/Nominal/nominal_primrec.ML` (diff)
The file was modified	`src/HOL/Nominal/nominal_thmdecls.ML` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/CLim.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HDeriv.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HLim.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HSEQ.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HSeries.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HTranscendental.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HyperDef.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HyperNat.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/NSA.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/NSCA.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/NSComplex.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/NatStar.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/StarDef.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/transfer_principle.ML` (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/Fib.thy` (diff)
The file was modified	`src/HOL/Orderings.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/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/Fin_Map.thy` (diff)
The file was modified	`src/HOL/Probability/Information.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/SPMF.thy` (diff)
The file was modified	`src/HOL/Probability/ex/Dining_Cryptographers.thy` (diff)
The file was modified	`src/HOL/Probability/ex/Measure_Not_CCC.thy` (diff)
The file was modified	`src/HOL/Prolog/Test.thy` (diff)
The file was modified	`src/HOL/Prolog/prolog.ML` (diff)
The file was modified	`src/HOL/Proofs/Lambda/Commutation.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/Eta.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/Lambda.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/NormalForm.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/StrongNorm.thy` (diff)
The file was modified	`src/HOL/Proofs/ex/Proof_Terms.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_Interfaces.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Examples/Quickcheck_Nesting.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/Real_Asymp/Eventuallize.thy` (diff)
The file was modified	`src/HOL/Real_Asymp/Inst_Existentials.thy` (diff)
The file was modified	`src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy` (diff)
The file was modified	`src/HOL/Real_Asymp/Multiseries_Expansion.thy` (diff)
The file was modified	`src/HOL/Real_Asymp/Real_Asymp_Approx.thy` (diff)
The file was modified	`src/HOL/Real_Asymp/Real_Asymp_Examples.thy` (diff)
The file was modified	`src/HOL/Real_Asymp/asymptotic_basis.ML` (diff)
The file was modified	`src/HOL/Real_Asymp/exp_log_expression.ML` (diff)
The file was modified	`src/HOL/Real_Asymp/multiseries_expansion.ML` (diff)
The file was modified	`src/HOL/Real_Asymp/multiseries_expansion_bounds.ML` (diff)
The file was modified	`src/HOL/Real_Asymp/real_asymp.ML` (diff)
The file was modified	`src/HOL/Real_Asymp/real_asymp_diag.ML` (diff)
The file was modified	`src/HOL/SET_Protocol/Cardholder_Registration.thy` (diff)
The file was modified	`src/HOL/SET_Protocol/Event_SET.thy` (diff)
The file was modified	`src/HOL/SET_Protocol/Merchant_Registration.thy` (diff)
The file was modified	`src/HOL/SET_Protocol/Message_SET.thy` (diff)
The file was modified	`src/HOL/SET_Protocol/Public_SET.thy` (diff)
The file was modified	`src/HOL/SET_Protocol/Purchase.thy` (diff)
The file was modified	`src/HOL/SMT_Examples/boogie.ML` (diff)
The file was modified	`src/HOL/SPARK/Manual/Reference.thy` (diff)
The file was modified	`src/HOL/Statespace/DistinctTreeProver.thy` (diff)
The file was modified	`src/HOL/Statespace/StateSpaceEx.thy` (diff)
The file was modified	`src/HOL/Statespace/StateSpaceSyntax.thy` (diff)
The file was modified	`src/HOL/Statespace/distinct_tree_prover.ML` (diff)
The file was modified	`src/HOL/Statespace/state_fun.ML` (diff)
The file was modified	`src/HOL/Statespace/state_space.ML` (diff)
The file was modified	`src/HOL/TLA/Action.thy` (diff)
The file was modified	`src/HOL/TLA/Buffer/DBuffer.thy` (diff)
The file was modified	`src/HOL/TLA/Inc/Inc.thy` (diff)
The file was modified	`src/HOL/TLA/Intensional.thy` (diff)
The file was modified	`src/HOL/TLA/Memory/MemClerk.thy` (diff)
The file was modified	`src/HOL/TLA/Memory/Memory.thy` (diff)
The file was modified	`src/HOL/TLA/Memory/MemoryImplementation.thy` (diff)
The file was modified	`src/HOL/TLA/Memory/RPC.thy` (diff)
The file was modified	`src/HOL/TLA/TLA.thy` (diff)
The file was modified	`src/HOL/TPTP/ATP_Theory_Export.thy` (diff)
The file was modified	`src/HOL/TPTP/MaSh_Eval.thy` (diff)
The file was modified	`src/HOL/TPTP/MaSh_Export_Base.thy` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Proof_Reconstruction.thy` (diff)
The file was modified	`src/HOL/TPTP/atp_problem_import.ML` (diff)
The file was modified	`src/HOL/TPTP/atp_theory_export.ML` (diff)
The file was modified	`src/HOL/TPTP/mash_export.ML` (diff)
The file was modified	`src/HOL/Tools/ATP/atp_problem_generate.ML` (diff)
The file was modified	`src/HOL/Tools/ATP/atp_proof_reconstruct.ML` (diff)
The file was modified	`src/HOL/Tools/ATP/atp_util.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_def_sugar.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_countable.ML` (diff)
The file was modified	`src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_def_code_dt.ML` (diff)
The file was modified	`src/HOL/Tools/Metis/metis_reconstruct.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_hol.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_model.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_mono.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_preproc.ML` (diff)
The file was modified	`src/HOL/Tools/Nunchaku/nunchaku.ML` (diff)
The file was modified	`src/HOL/Tools/Nunchaku/nunchaku_collect.ML` (diff)
The file was modified	`src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_replay_methods.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_util.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smtlib_interface.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smtlib_proof.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/verit_proof.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/z3_interface.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/z3_replay_methods.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML` (diff)
The file was modified	`src/HOL/Tools/Transfer/transfer.ML` (diff)
The file was modified	`src/HOL/Tools/set_comprehension_pointfree.ML` (diff)
The file was modified	`src/HOL/Transitive_Closure.thy` (diff)
The file was modified	`src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy` (diff)
The file was modified	`src/HOL/Types_To_Sets/Examples/Prerequisites.thy` (diff)
The file was modified	`src/HOL/Types_To_Sets/Examples/T2_Spaces.thy` (diff)
The file was modified	`src/HOL/Types_To_Sets/internalize_sort.ML` (diff)
The file was modified	`src/HOL/Types_To_Sets/local_typedef.ML` (diff)
The file was modified	`src/HOL/Types_To_Sets/unoverload_type.ML` (diff)
The file was modified	`src/HOL/Types_To_Sets/unoverloading.ML` (diff)
The file was modified	`src/HOL/UNITY/Comp/Alloc.thy` (diff)
The file was modified	`src/HOL/UNITY/Comp/Priority.thy` (diff)
The file was modified	`src/HOL/UNITY/Comp/Progress.thy` (diff)
The file was modified	`src/HOL/UNITY/Extend.thy` (diff)
The file was modified	`src/HOL/UNITY/Lift_prog.thy` (diff)
The file was modified	`src/HOL/UNITY/PPROD.thy` (diff)
The file was modified	`src/HOL/UNITY/ProgressSets.thy` (diff)
The file was modified	`src/HOL/UNITY/Simple/NSP_Bad.thy` (diff)
The file was modified	`src/HOL/UNITY/Transformers.thy` (diff)
The file was modified	`src/HOL/UNITY/UNITY.thy` (diff)
The file was modified	`src/HOL/UNITY/Union.thy` (diff)
The file was modified	`src/HOL/UNITY/WFair.thy` (diff)
The file was modified	`src/HOL/Unix/Nested_Environment.thy` (diff)
The file was modified	`src/HOL/Unix/Unix.thy` (diff)
The file was modified	`src/HOL/Word/Tools/smt_word.ML` (diff)
The file was modified	`src/HOL/Word/Tools/word_lib.ML` (diff)
The file was modified	`src/HOL/Word/WordBitwise.thy` (diff)
The file was modified	`src/HOL/ex/Adhoc_Overloading_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Antiquote.thy` (diff)
The file was modified	`src/HOL/ex/Arith_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Ballot.thy` (diff)
The file was modified	`src/HOL/ex/CTL.thy` (diff)
The file was modified	`src/HOL/ex/Cartouche_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Classical.thy` (diff)
The file was modified	`src/HOL/ex/Code_Lazy_Demo.thy` (diff)
The file was modified	`src/HOL/ex/Code_Timing.thy` (diff)
The file was modified	`src/HOL/ex/Commands.thy` (diff)
The file was modified	`src/HOL/ex/Computations.thy` (diff)
The file was modified	`src/HOL/ex/Datatype_Record_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Dedekind_Real.thy` (diff)
The file was modified	`src/HOL/ex/Erdoes_Szekeres.thy` (diff)
The file was modified	`src/HOL/ex/Execute_Choice.thy` (diff)
The file was modified	`src/HOL/ex/Function_Growth.thy` (diff)
The file was modified	`src/HOL/ex/Groebner_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Hex_Bin_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Iff_Oracle.thy` (diff)
The file was modified	`src/HOL/ex/LocaleTest2.thy` (diff)
The file was modified	`src/HOL/ex/ML.thy` (diff)
The file was modified	`src/HOL/ex/Meson_Test.thy` (diff)
The file was modified	`src/HOL/ex/Multiquote.thy` (diff)
The file was modified	`src/HOL/ex/PER.thy` (diff)
The file was modified	`src/HOL/ex/Primrec.thy` (diff)
The file was modified	`src/HOL/ex/Radix_Sort.thy` (diff)
The file was modified	`src/HOL/ex/Records.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/SAT_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Simproc_Tests.thy` (diff)
The file was modified	`src/HOL/ex/Sorting_Algorithms_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Sum_of_Powers.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/Tree23.thy` (diff)
The file was modified	`src/HOL/ex/While_Combinator_Example.thy` (diff)
The file was modified	`src/HOL/ex/veriT_Preprocessing.thy` (diff)
The file was modified	`src/Tools/Code/code_runtime.ML` (diff)
The file was modified	`src/ZF/Inductive.thy` (diff)
The file was modified	`src/ZF/Tools/datatype_package.ML` (diff)
The file was modified	`src/ZF/Tools/inductive_package.ML` (diff)
The file was modified	`src/ZF/ind_syntax.ML` (diff)
The file was modified	`src/ZF/int_arith.ML` (diff)
Changeset 69596:c8a2755bf220 by wenzelm: latex macro for \<^const>;
The file was modified	`lib/texinputs/isabellesym.sty` (diff)
Changeset 69595:ec135235fbcc by wenzelm: mark for isabelle update -u control_cartouches;
The file was modified	`src/Pure/ML/ml_antiquotations.ML` (diff)
Changeset 69594:1d340f7f8dce by wenzelm: proper session base foundations (amending e848328cb2c1);
The file was modified	`src/Pure/PIDE/headless.scala` (diff)