Changes

Summary

isabelle update_cartouches -c -t;
tuned spelling;

Changeset 63167:0909deb8059b by wenzelm: isabelle update_cartouches -c -t;
The file was modified	`src/HOL/Algebra/AbelCoset.thy` (diff)
The file was modified	`src/HOL/Algebra/Bij.thy` (diff)
The file was modified	`src/HOL/Algebra/Congruence.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/FiniteProduct.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/Lattice.thy` (diff)
The file was modified	`src/HOL/Algebra/QuotRing.thy` (diff)
The file was modified	`src/HOL/Algebra/Ring.thy` (diff)
The file was modified	`src/HOL/Algebra/RingHom.thy` (diff)
The file was modified	`src/HOL/Algebra/Sylow.thy` (diff)
The file was modified	`src/HOL/Algebra/UnivPoly.thy` (diff)
The file was modified	`src/HOL/Cardinals/Bounded_Set.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/Cardinals.thy` (diff)
The file was modified	`src/HOL/Cardinals/Fun_More.thy` (diff)
The file was modified	`src/HOL/Cardinals/Order_Relation_More.thy` (diff)
The file was modified	`src/HOL/Cardinals/Order_Union.thy` (diff)
The file was modified	`src/HOL/Cardinals/Ordinal_Arithmetic.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_Extension.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_OCaml.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/Corec_Examples/LFilter.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Compat.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Derivation_Trees/DTree.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/Parallel.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/Lift_BNF.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/Misc_Primcorec.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Misc_Primrec.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/TreeFI.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/TreeFsetI.thy` (diff)
The file was modified	`src/HOL/IMPP/Com.thy` (diff)
The file was modified	`src/HOL/IMPP/EvenOdd.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/Asig.thy` (diff)
The file was modified	`src/HOL/IOA/IOA.thy` (diff)
The file was modified	`src/HOL/IOA/Solve.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/Array.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/Imperative_HOL.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/Imperative_HOL_ex.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/Overview.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/Ref.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/ex/Imperative_Reverse.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/Imperative_HOL/ex/Sorted_List.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/ex/Subarray.thy` (diff)
The file was modified	`src/HOL/Import/HOL_Light_Import.thy` (diff)
The file was modified	`src/HOL/Import/HOL_Light_Maps.thy` (diff)
The file was modified	`src/HOL/Import/Import_Setup.thy` (diff)
The file was modified	`src/HOL/Induct/ABexp.thy` (diff)
The file was modified	`src/HOL/Induct/Com.thy` (diff)
The file was modified	`src/HOL/Induct/Common_Patterns.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/Induct/Sigma_Algebra.thy` (diff)
The file was modified	`src/HOL/Matrix_LP/ComputeFloat.thy` (diff)
The file was modified	`src/HOL/Matrix_LP/ComputeHOL.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/Binary_Tree.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Clausification.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Message.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Proxies.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Sets.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Tarski.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Trans_Closure.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Type_Encodings.thy` (diff)
The file was modified	`src/HOL/Mirabelle/Mirabelle.thy` (diff)
The file was modified	`src/HOL/Mirabelle/Mirabelle_Test.thy` (diff)
The file was modified	`src/HOL/Mirabelle/ex/Ex.thy` (diff)
The file was modified	`src/HOL/Mutabelle/MutabelleExtra.thy` (diff)
The file was modified	`src/HOL/NanoJava/AxSem.thy` (diff)
The file was modified	`src/HOL/NanoJava/Decl.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/NanoJava/Term.thy` (diff)
The file was modified	`src/HOL/NanoJava/TypeRel.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Core_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Datatype_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Hotel_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Induct_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Integer_Nits.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/Pattern_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Record_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Refute_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Special_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Tests_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Typedef_Nits.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/CK_Machine.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/CR.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/Class2.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Class3.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/SN.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/Number_Theory/Cong.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Euclidean_Algorithm.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Fib.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Residues.thy` (diff)
The file was modified	`src/HOL/Old_Number_Theory/Chinese.thy` (diff)
The file was modified	`src/HOL/Old_Number_Theory/EulerFermat.thy` (diff)
The file was modified	`src/HOL/Old_Number_Theory/Fib.thy` (diff)
The file was modified	`src/HOL/Old_Number_Theory/IntFact.thy` (diff)
The file was modified	`src/HOL/Old_Number_Theory/IntPrimes.thy` (diff)
The file was modified	`src/HOL/Old_Number_Theory/Legacy_GCD.thy` (diff)
The file was modified	`src/HOL/Old_Number_Theory/WilsonBij.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.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/Hotel_Example_Small_Generator.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/Borel_Space.thy` (diff)
The file was modified	`src/HOL/Probability/Characteristic_Functions.thy` (diff)
The file was modified	`src/HOL/Probability/Distribution_Functions.thy` (diff)
The file was modified	`src/HOL/Probability/Levy.thy` (diff)
The file was modified	`src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy` (diff)
The file was modified	`src/HOL/Probability/Sigma_Algebra.thy` (diff)
The file was modified	`src/HOL/Probability/Sinc_Integral.thy` (diff)
The file was modified	`src/HOL/Prolog/Func.thy` (diff)
The file was modified	`src/HOL/Prolog/HOHH.thy` (diff)
The file was modified	`src/HOL/Prolog/Test.thy` (diff)
The file was modified	`src/HOL/Prolog/Type.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Examples/Completeness.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/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/Quotient_Examples/DList.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/FSet.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/Int_Pow.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/Lift_DList.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/Lift_FSet.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/Lift_Fun.thy` (diff)
The file was modified	`src/HOL/Quotient_Examples/Lift_Set.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/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.thy` (diff)
The file was modified	`src/HOL/SMT_Examples/SMT_Examples.thy` (diff)
The file was modified	`src/HOL/SMT_Examples/SMT_Tests.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/Hash.thy` (diff)
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy` (diff)
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/R_R.thy` (diff)
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/Round.thy` (diff)
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy` (diff)
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/S_R.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/Reference.thy` (diff)
The file was modified	`src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy` (diff)
The file was modified	`src/HOL/SPARK/Manual/VC_Principles.thy` (diff)
The file was modified	`src/HOL/SPARK/SPARK.thy` (diff)
The file was modified	`src/HOL/SPARK/SPARK_Setup.thy` (diff)
The file was modified	`src/HOL/Statespace/DistinctTreeProver.thy` (diff)
The file was modified	`src/HOL/Statespace/StateFun.thy` (diff)
The file was modified	`src/HOL/Statespace/StateSpaceEx.thy` (diff)
The file was modified	`src/HOL/Statespace/StateSpaceLocale.thy` (diff)
The file was modified	`src/HOL/Statespace/StateSpaceSyntax.thy` (diff)
The file was modified	`src/HOL/TPTP/ATP_Problem_Import.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.thy` (diff)
The file was modified	`src/HOL/TPTP/MaSh_Export_Base.thy` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Interpret_Test.thy` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Parser.thy` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Parser_Example.thy` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Parser_Test.thy` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Proof_Reconstruction.thy` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Test.thy` (diff)
The file was modified	`src/HOL/ZF/HOLZF.thy` (diff)
Changeset 63166:143f58bb34f9 by wenzelm: tuned spelling;
The file was modified	`NEWS` (diff)