Changes

Summary

typo
tuned notation
tuned
ran isabelle update_op on all sources
Manual updates towards conversion of "op" syntax
tuned op
tuned op's

Changeset 67402:b71431a2051e by nipkow: typo
The file was modified	`NEWS` (diff)
Changeset 67401:a82df75b7f85 by nipkow: tuned notation
The file was modified	`src/HOL/Orderings.thy` (diff)
The file was modified	`src/HOL/Set.thy` (diff)
Changeset 67400:bbed46f40cf5 by nipkow: tuned
The file was modified	`NEWS` (diff)
Changeset 67399:eab6ce8368fa by nipkow: ran isabelle update_op on all sources
The file was modified	`src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy` (diff)
The file was modified	`src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy` (diff)
The file was modified	`src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy` (diff)
The file was modified	`src/Benchmarks/Record_Benchmark/Record_Benchmark.thy` (diff)
The file was modified	`src/CTT/CTT.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/Preface.thy` (diff)
The file was modified	`src/Doc/How_to_Prove_it/How_to_Prove_it.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/Proof_Script.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Symbols.thy` (diff)
The file was modified	`src/Doc/JEdit/JEdit.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/Main/Main_Doc.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/Basics.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/LaTeXsugar.thy` (diff)
The file was modified	`src/Doc/System/Environment.thy` (diff)
The file was modified	`src/Doc/System/Misc.thy` (diff)
The file was modified	`src/Doc/System/Presentation.thy` (diff)
The file was modified	`src/Doc/Tutorial/Types/Pairs.thy` (diff)
The file was modified	`src/FOL/ex/Locale_Test/Locale_Test1.thy` (diff)
The file was modified	`src/FOLP/IFOLP.thy` (diff)
The file was modified	`src/HOL/Algebra/Complete_Lattice.thy` (diff)
The file was modified	`src/HOL/Algebra/Divisibility.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/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/Sylow.thy` (diff)
The file was modified	`src/HOL/Algebra/UnivPoly.thy` (diff)
The file was modified	`src/HOL/Analysis/Ball_Volume.thy` (diff)
The file was modified	`src/HOL/Analysis/Binary_Product_Measure.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/Brouwer_Fixpoint.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_Analysis_Basics.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/Convex_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Derivative.thy` (diff)
The file was modified	`src/HOL/Analysis/Determinants.thy` (diff)
The file was modified	`src/HOL/Analysis/Embed_Measure.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/Finite_Cartesian_Product.thy` (diff)
The file was modified	`src/HOL/Analysis/Finite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Further_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Gamma_Function.thy` (diff)
The file was modified	`src/HOL/Analysis/Great_Picard.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/Homeomorphism.thy` (diff)
The file was modified	`src/HOL/Analysis/Improper_Integral.thy` (diff)
The file was modified	`src/HOL/Analysis/Inner_Product.thy` (diff)
The file was modified	`src/HOL/Analysis/Lebesgue_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Linear_Algebra.thy` (diff)
The file was modified	`src/HOL/Analysis/Measure_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Path_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Polytope.thy` (diff)
The file was modified	`src/HOL/Analysis/Riemann_Mapping.thy` (diff)
The file was modified	`src/HOL/Analysis/Set_Integral.thy` (diff)
The file was modified	`src/HOL/Analysis/Sigma_Algebra.thy` (diff)
The file was modified	`src/HOL/Analysis/Starlike.thy` (diff)
The file was modified	`src/HOL/Analysis/Tagged_Division.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/normarith.ML` (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/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/State.thy` (diff)
The file was modified	`src/HOL/Basic_BNF_LFPs.thy` (diff)
The file was modified	`src/HOL/Basic_BNFs.thy` (diff)
The file was modified	`src/HOL/Binomial.thy` (diff)
The file was modified	`src/HOL/Cardinals/Bounded_Set.thy` (diff)
The file was modified	`src/HOL/Code_Numeral.thy` (diff)
The file was modified	`src/HOL/Complete_Lattices.thy` (diff)
The file was modified	`src/HOL/Complete_Partial_Order.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Euclidean_Algorithm.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Formal_Power_Series.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Nth_Powers.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/Squarefree.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/Misc_Mono.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Base_FDS.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Binomial_Heap.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Sorted_Less.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/Parallel_Composition.thy` (diff)
The file was modified	`src/HOL/Datatype_Examples/Stream_Processor.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Algebra_Aux.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/Decision_Procs/Polynomial_List.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/approximation.ML` (diff)
The file was modified	`src/HOL/Decision_Procs/langford.ML` (diff)
The file was modified	`src/HOL/Deriv.thy` (diff)
The file was modified	`src/HOL/Enum.thy` (diff)
The file was modified	`src/HOL/Equiv_Relations.thy` (diff)
The file was modified	`src/HOL/Factorial.thy` (diff)
The file was modified	`src/HOL/Filter.thy` (diff)
The file was modified	`src/HOL/Fun.thy` (diff)
The file was modified	`src/HOL/GCD.thy` (diff)
The file was modified	`src/HOL/Groups_List.thy` (diff)
The file was modified	`src/HOL/HOL.thy` (diff)
The file was modified	`src/HOL/HOLCF/Cpodef.thy` (diff)
The file was modified	`src/HOL/HOLCF/Discrete.thy` (diff)
The file was modified	`src/HOL/HOLCF/Domain.thy` (diff)
The file was modified	`src/HOL/HOLCF/Fun_Cpo.thy` (diff)
The file was modified	`src/HOL/HOLCF/Library/List_Cpo.thy` (diff)
The file was modified	`src/HOL/HOLCF/Product_Cpo.thy` (diff)
The file was modified	`src/HOL/HOLCF/Universal.thy` (diff)
The file was modified	`src/HOL/HOLCF/Up.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int2_ivl.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int3.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_State.thy` (diff)
The file was modified	`src/HOL/IMP/Collecting.thy` (diff)
The file was modified	`src/HOL/IMP/Compiler2.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/Heap_Monad.thy` (diff)
The file was modified	`src/HOL/Import/HOL_Light_Maps.thy` (diff)
The file was modified	`src/HOL/Int.thy` (diff)
The file was modified	`src/HOL/Lattices.thy` (diff)
The file was modified	`src/HOL/Library/BNF_Corec.thy` (diff)
The file was modified	`src/HOL/Library/Cancellation.thy` (diff)
The file was modified	`src/HOL/Library/Cardinality.thy` (diff)
The file was modified	`src/HOL/Library/Char_ord.thy` (diff)
The file was modified	`src/HOL/Library/Code_Real_Approx_By_Float.thy` (diff)
The file was modified	`src/HOL/Library/Complete_Partial_Order2.thy` (diff)
The file was modified	`src/HOL/Library/Conditional_Parametricity.thy` (diff)
The file was modified	`src/HOL/Library/Countable.thy` (diff)
The file was modified	`src/HOL/Library/Countable_Set.thy` (diff)
The file was modified	`src/HOL/Library/Countable_Set_Type.thy` (diff)
The file was modified	`src/HOL/Library/DAList_Multiset.thy` (diff)
The file was modified	`src/HOL/Library/Diagonal_Subsequence.thy` (diff)
The file was modified	`src/HOL/Library/Discrete.thy` (diff)
The file was modified	`src/HOL/Library/Disjoint_Sets.thy` (diff)
The file was modified	`src/HOL/Library/Dlist.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Nonnegative_Real.thy` (diff)
The file was modified	`src/HOL/Library/FSet.thy` (diff)
The file was modified	`src/HOL/Library/Finite_Map.thy` (diff)
The file was modified	`src/HOL/Library/Float.thy` (diff)
The file was modified	`src/HOL/Library/LaTeXsugar.thy` (diff)
The file was modified	`src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy` (diff)
The file was modified	`src/HOL/Library/ListVector.thy` (diff)
The file was modified	`src/HOL/Library/Mapping.thy` (diff)
The file was modified	`src/HOL/Library/More_List.thy` (diff)
The file was modified	`src/HOL/Library/Multiset_Permutations.thy` (diff)
The file was modified	`src/HOL/Library/Nat_Bijection.thy` (diff)
The file was modified	`src/HOL/Library/Numeral_Type.thy` (diff)
The file was modified	`src/HOL/Library/Open_State_Syntax.thy` (diff)
The file was modified	`src/HOL/Library/Pattern_Aliases.thy` (diff)
The file was modified	`src/HOL/Library/Perm.thy` (diff)
The file was modified	`src/HOL/Library/Permutations.thy` (diff)
The file was modified	`src/HOL/Library/Predicate_Compile_Alternative_Defs.thy` (diff)
The file was modified	`src/HOL/Library/Quotient_List.thy` (diff)
The file was modified	`src/HOL/Library/Quotient_Product.thy` (diff)
The file was modified	`src/HOL/Library/Quotient_Set.thy` (diff)
The file was modified	`src/HOL/Library/Quotient_Sum.thy` (diff)
The file was modified	`src/HOL/Library/RBT_Set.thy` (diff)
The file was modified	`src/HOL/Library/State_Monad.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/Subseq_Order.thy` (diff)
The file was modified	`src/HOL/Library/Sum_of_Squares/sum_of_squares.ML` (diff)
The file was modified	`src/HOL/Library/Tree.thy` (diff)
The file was modified	`src/HOL/Library/Tree_Real.thy` (diff)
The file was modified	`src/HOL/Library/Uprod.thy` (diff)
The file was modified	`src/HOL/Library/conditional_parametricity.ML` (diff)
The file was modified	`src/HOL/Library/positivstellensatz.ML` (diff)
The file was modified	`src/HOL/Library/refute.ML` (diff)
The file was modified	`src/HOL/Lifting.thy` (diff)
The file was modified	`src/HOL/Lifting_Set.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/Matrix_LP/Cplex_tools.ML` (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/Proxies.thy` (diff)
The file was modified	`src/HOL/MicroJava/BV/BVExample.thy` (diff)
The file was modified	`src/HOL/MicroJava/BV/Typing_Framework_JVM.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/Listn.thy` (diff)
The file was modified	`src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML` (diff)
The file was modified	`src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML` (diff)
The file was modified	`src/HOL/NanoJava/Equivalence.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/Nitpick_Examples/Core_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/Refute_Nits.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Standardization.thy` (diff)
The file was modified	`src/HOL/Nominal/nominal_datatype.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/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/HLog.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HyperDef.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/Num.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/Totient.thy` (diff)
The file was modified	`src/HOL/Option.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/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/Predicate_Compile_Tests.thy` (diff)
The file was modified	`src/HOL/Probability/Distributions.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/Independent_Family.thy` (diff)
The file was modified	`src/HOL/Probability/Infinite_Product_Measure.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/Stream_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/Test.thy` (diff)
The file was modified	`src/HOL/Proofs/Extraction/Higman_Extraction.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/ListApplication.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/Standardization.thy` (diff)
The file was modified	`src/HOL/Proofs/ex/Proof_Terms.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Narrowing.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Random.thy` (diff)
The file was modified	`src/HOL/Quotient.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/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_Rat.thy` (diff)
The file was modified	`src/HOL/Real.thy` (diff)
The file was modified	`src/HOL/Real_Vector_Spaces.thy` (diff)
The file was modified	`src/HOL/Relation.thy` (diff)
The file was modified	`src/HOL/SMT.thy` (diff)
The file was modified	`src/HOL/SMT_Examples/SMT_Examples.thy` (diff)
The file was modified	`src/HOL/SMT_Examples/boogie.ML` (diff)
The file was modified	`src/HOL/SPARK/SPARK.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/TLA/Intensional.thy` (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/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/Tools/ATP/atp_problem.ML` (diff)
The file was modified	`src/HOL/Tools/ATP/atp_problem_generate.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_def_tactics.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.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_tactics.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_lfp_tactics.ML` (diff)
The file was modified	`src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_info.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_commands.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_mono.ML` (diff)
The file was modified	`src/HOL/Tools/Nunchaku/nunchaku_collect.ML` (diff)
The file was modified	`src/HOL/Tools/Nunchaku/nunchaku_commands.ML` (diff)
The file was modified	`src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/code_prolog.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/core_data.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML` (diff)
The file was modified	`src/HOL/Tools/Qelim/cooper.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_systems.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smtlib.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smtlib_interface.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML` (diff)
The file was modified	`src/HOL/Tools/Transfer/transfer.ML` (diff)
The file was modified	`src/HOL/Tools/datatype_realizer.ML` (diff)
The file was modified	`src/HOL/Tools/functor.ML` (diff)
The file was modified	`src/HOL/Tools/groebner.ML` (diff)
The file was modified	`src/HOL/Tools/rewrite_hol_proof.ML` (diff)
The file was modified	`src/HOL/Tools/sat_solver.ML` (diff)
The file was modified	`src/HOL/Tools/semiring_normalizer.ML` (diff)
The file was modified	`src/HOL/Tools/set_comprehension_pointfree.ML` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)
The file was modified	`src/HOL/Transfer.thy` (diff)
The file was modified	`src/HOL/Transitive_Closure.thy` (diff)
The file was modified	`src/HOL/Types_To_Sets/Examples/Finite.thy` (diff)
The file was modified	`src/HOL/Types_To_Sets/Examples/T2_Spaces.thy` (diff)
The file was modified	`src/HOL/Wellfounded.thy` (diff)
The file was modified	`src/HOL/Word/Bool_List_Representation.thy` (diff)
The file was modified	`src/HOL/Word/Misc_Typedef.thy` (diff)
The file was modified	`src/HOL/Word/Word.thy` (diff)
The file was modified	`src/HOL/Word/WordBitwise.thy` (diff)
The file was modified	`src/HOL/Zorn.thy` (diff)
The file was modified	`src/HOL/ex/Ballot.thy` (diff)
The file was modified	`src/HOL/ex/Coercion_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Conditional_Parametricity_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Erdoes_Szekeres.thy` (diff)
The file was modified	`src/HOL/ex/LocaleTest2.thy` (diff)
The file was modified	`src/HOL/ex/Refute_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Transfer_Debug.thy` (diff)
The file was modified	`src/HOL/ex/Transfer_Int_Nat.thy` (diff)
The file was modified	`src/HOL/ex/While_Combinator_Example.thy` (diff)
The file was modified	`src/ZF/Constructible/Rank.thy` (diff)
The file was modified	`src/ZF/Constructible/Rank_Separation.thy` (diff)
The file was modified	`src/ZF/Induct/FoldSet.thy` (diff)
The file was modified	`src/ZF/Order.thy` (diff)
The file was modified	`src/ZF/Perm.thy` (diff)
The file was modified	`src/ZF/UNITY/Follows.thy` (diff)
The file was modified	`src/ZF/UNITY/Monotonicity.thy` (diff)
The file was modified	`src/ZF/UNITY/MultisetSum.thy` (diff)
The file was modified	`src/ZF/UNITY/Mutex.thy` (diff)
The file was modified	`src/ZF/ex/Limit.thy` (diff)
Changeset 67398:5eb932e604a2 by nipkow: Manual updates towards conversion of "op" syntax
The file was added	`lib/Tools/update_op`
The file was modified	`NEWS` (diff)
The file was modified	`src/Doc/Isar_Ref/Inner_Syntax.thy` (diff)
The file was modified	`src/Doc/Locales/Examples.thy` (diff)
The file was modified	`src/Doc/Locales/Examples3.thy` (diff)
The file was modified	`src/Doc/Tutorial/Documents/Documents.thy` (diff)
The file was modified	`src/HOL/Algebra/Ring.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Dense_Linear_Order.thy` (diff)
The file was modified	`src/HOL/Library/Multiset.thy` (diff)
The file was modified	`src/HOL/Library/Preorder.thy` (diff)
The file was modified	`src/HOL/Orderings.thy` (diff)
The file was modified	`src/HOL/Set.thy` (diff)
The file was modified	`src/Pure/Syntax/mixfix.ML` (diff)
The file was modified	`src/ZF/ex/Ring.thy` (diff)
Changeset 67397:12b0c11e3d20 by nipkow: tuned op
The file was modified	`src/HOL/Decision_Procs/Algebra_Aux.thy` (diff)
Changeset 67396:172a02125bfa by nipkow: tuned op's
The file was modified	`src/HOL/Algebra/IntRing.thy` (diff)
The file was modified	`src/HOL/Algebra/UnivPoly.thy` (diff)
The file was modified	`src/HOL/Analysis/Cauchy_Integral_Theorem.thy` (diff)