Changes

Summary

more symbols;
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;

Changeset 67091:1393c2340eec by wenzelm: more symbols;
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/Complete_Lattice.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/FiniteProduct.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/Lattice.thy` (diff)
The file was modified	`src/HOL/Algebra/Order.thy` (diff)
The file was modified	`src/HOL/Algebra/Ring.thy` (diff)
The file was modified	`src/HOL/Algebra/UnivPoly.thy` (diff)
The file was modified	`src/HOL/BNF_Cardinal_Order_Relation.thy` (diff)
The file was modified	`src/HOL/BNF_Composition.thy` (diff)
The file was modified	`src/HOL/BNF_Def.thy` (diff)
The file was modified	`src/HOL/BNF_Fixpoint_Base.thy` (diff)
The file was modified	`src/HOL/BNF_Greatest_Fixpoint.thy` (diff)
The file was modified	`src/HOL/BNF_Least_Fixpoint.thy` (diff)
The file was modified	`src/HOL/BNF_Wellorder_Constructions.thy` (diff)
The file was modified	`src/HOL/BNF_Wellorder_Embedding.thy` (diff)
The file was modified	`src/HOL/Basic_BNFs.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/Conditionally_Complete_Lattices.thy` (diff)
The file was modified	`src/HOL/Divides.thy` (diff)
The file was modified	`src/HOL/Enum.thy` (diff)
The file was modified	`src/HOL/Fields.thy` (diff)
The file was modified	`src/HOL/Groebner_Basis.thy` (diff)
The file was modified	`src/HOL/HOL.thy` (diff)
The file was modified	`src/HOL/Library/BNF_Corec.thy` (diff)
The file was modified	`src/HOL/Library/Cardinality.thy` (diff)
The file was modified	`src/HOL/Library/DAList.thy` (diff)
The file was modified	`src/HOL/Library/Diagonal_Subsequence.thy` (diff)
The file was modified	`src/HOL/Library/Extended.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Nat.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Real.thy` (diff)
The file was modified	`src/HOL/Library/FSet.thy` (diff)
The file was modified	`src/HOL/Library/Old_Datatype.thy` (diff)
The file was modified	`src/HOL/Library/Old_Recdef.thy` (diff)
The file was modified	`src/HOL/Library/Option_ord.thy` (diff)
The file was modified	`src/HOL/Library/Predicate_Compile_Alternative_Defs.thy` (diff)
The file was modified	`src/HOL/Library/Product_Order.thy` (diff)
The file was modified	`src/HOL/Library/RBT_Set.thy` (diff)
The file was modified	`src/HOL/Library/Ramsey.thy` (diff)
The file was modified	`src/HOL/Library/Stream.thy` (diff)
The file was modified	`src/HOL/Library/Sublist.thy` (diff)
The file was modified	`src/HOL/Library/Sum_of_Squares/sum_of_squares.ML` (diff)
The file was modified	`src/HOL/Library/While_Combinator.thy` (diff)
The file was modified	`src/HOL/Library/positivstellensatz.ML` (diff)
The file was modified	`src/HOL/Limited_Sequence.thy` (diff)
The file was modified	`src/HOL/Limits.thy` (diff)
The file was modified	`src/HOL/List.thy` (diff)
The file was modified	`src/HOL/MacLaurin.thy` (diff)
The file was modified	`src/HOL/Map.thy` (diff)
The file was modified	`src/HOL/Meson.thy` (diff)
The file was modified	`src/HOL/Nat.thy` (diff)
The file was modified	`src/HOL/Nitpick.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HTranscendental.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HyperNat.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/NSCA.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/NatStar.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Euler_Criterion.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Gauss.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Pocklington.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Residues.thy` (diff)
The file was modified	`src/HOL/Numeral_Simprocs.thy` (diff)
The file was modified	`src/HOL/Option.thy` (diff)
The file was modified	`src/HOL/Orderings.thy` (diff)
The file was modified	`src/HOL/Partial_Function.thy` (diff)
The file was modified	`src/HOL/Predicate.thy` (diff)
The file was modified	`src/HOL/Presburger.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Exhaustive.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Narrowing.thy` (diff)
The file was modified	`src/HOL/Quotient.thy` (diff)
The file was modified	`src/HOL/Random_Pred.thy` (diff)
The file was modified	`src/HOL/Random_Sequence.thy` (diff)
The file was modified	`src/HOL/Record.thy` (diff)
The file was modified	`src/HOL/SMT.thy` (diff)
The file was modified	`src/HOL/Set.thy` (diff)
The file was modified	`src/HOL/Set_Interval.thy` (diff)
The file was modified	`src/HOL/String.thy` (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/Argo/argo_real.ML` (diff)
The file was modified	`src/HOL/Tools/Argo/argo_tactic.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_comp.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_util.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_gfp.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_tactics.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lift.ML` (diff)
The file was modified	`src/HOL/Tools/Meson/meson.ML` (diff)
The file was modified	`src/HOL/Tools/Meson/meson_clausify.ML` (diff)
The file was modified	`src/HOL/Tools/Metis/metis_reconstruct.ML` (diff)
The file was modified	`src/HOL/Tools/Old_Datatype/old_datatype.ML` (diff)
The file was modified	`src/HOL/Tools/Quotient/quotient_tacs.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/conj_disj_perm.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/z3_replay.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/z3_replay_methods.ML` (diff)
The file was modified	`src/HOL/Tools/cnf.ML` (diff)
The file was modified	`src/HOL/Tools/inductive.ML` (diff)
The file was modified	`src/HOL/Tools/rewrite_hol_proof.ML` (diff)
The file was modified	`src/HOL/Tools/sat.ML` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)
Changeset 67090:0ec94bb9cec4 by wenzelm: clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
The file was modified	`src/Pure/Isar/keyword.scala` (diff)