Changes

Summary

isabelle update -u control_cartouches;
support for isabelle update -u control_cartouches;

Changeset 69593:3dda49e08b9d by wenzelm: isabelle update -u control_cartouches;
The file was modified	`src/CCL/CCL.thy` (diff)
The file was modified	`src/CCL/Term.thy` (diff)
The file was modified	`src/CCL/Type.thy` (diff)
The file was modified	`src/CCL/Wfd.thy` (diff)
The file was modified	`src/CCL/ex/Stream.thy` (diff)
The file was modified	`src/CTT/CTT.thy` (diff)
The file was modified	`src/CTT/ex/Elimination.thy` (diff)
The file was modified	`src/CTT/ex/Equality.thy` (diff)
The file was modified	`src/CTT/ex/Synthesis.thy` (diff)
The file was modified	`src/Cube/Cube.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/First_Order_Logic.thy` (diff)
The file was modified	`src/Doc/Logics_ZF/IFOL_examples.thy` (diff)
The file was modified	`src/Doc/Logics_ZF/ZF_Isar.thy` (diff)
The file was modified	`src/Doc/System/Environment.thy` (diff)
The file was modified	`src/Doc/System/Server.thy` (diff)
The file was modified	`src/Doc/System/Sessions.thy` (diff)
The file was modified	`src/Doc/antiquote_setup.ML` (diff)
The file was modified	`src/FOL/FOL.thy` (diff)
The file was modified	`src/FOL/IFOL.thy` (diff)
The file was modified	`src/FOL/ex/Intuitionistic.thy` (diff)
The file was modified	`src/FOL/ex/Locale_Test/Locale_Test1.thy` (diff)
The file was modified	`src/FOL/ex/Miniscope.thy` (diff)
The file was modified	`src/FOL/ex/Prolog.thy` (diff)
The file was modified	`src/FOL/ex/Propositional_Cla.thy` (diff)
The file was modified	`src/FOL/ex/Propositional_Int.thy` (diff)
The file was modified	`src/FOL/ex/Quantifiers_Int.thy` (diff)
The file was modified	`src/FOL/fologic.ML` (diff)
The file was modified	`src/FOL/simpdata.ML` (diff)
The file was modified	`src/FOLP/FOLP.thy` (diff)
The file was modified	`src/FOLP/IFOLP.thy` (diff)
The file was modified	`src/FOLP/ex/Classical.thy` (diff)
The file was modified	`src/FOLP/ex/If.thy` (diff)
The file was modified	`src/FOLP/ex/Intro.thy` (diff)
The file was modified	`src/FOLP/ex/Intuitionistic.thy` (diff)
The file was modified	`src/FOLP/ex/Nat.thy` (diff)
The file was modified	`src/FOLP/ex/Propositional_Cla.thy` (diff)
The file was modified	`src/FOLP/ex/Propositional_Int.thy` (diff)
The file was modified	`src/FOLP/ex/Quantifiers_Cla.thy` (diff)
The file was modified	`src/FOLP/ex/Quantifiers_Int.thy` (diff)
The file was modified	`src/FOLP/hypsubst.ML` (diff)
The file was modified	`src/FOLP/simp.ML` (diff)
The file was modified	`src/FOLP/simpdata.ML` (diff)
The file was modified	`src/HOL/BNF_Wellorder_Relation.thy` (diff)
The file was modified	`src/HOL/Binomial.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/Conditionally_Complete_Lattices.thy` (diff)
The file was modified	`src/HOL/Deriv.thy` (diff)
The file was modified	`src/HOL/Divides.thy` (diff)
The file was modified	`src/HOL/Eisbach/Eisbach_Tools.thy` (diff)
The file was modified	`src/HOL/Eisbach/eisbach_rule_insts.ML` (diff)
The file was modified	`src/HOL/Eisbach/match_method.ML` (diff)
The file was modified	`src/HOL/Eisbach/method_closure.ML` (diff)
The file was modified	`src/HOL/Enum.thy` (diff)
The file was modified	`src/HOL/Euclidean_Division.thy` (diff)
The file was modified	`src/HOL/Extraction.thy` (diff)
The file was modified	`src/HOL/Fields.thy` (diff)
The file was modified	`src/HOL/Filter.thy` (diff)
The file was modified	`src/HOL/Finite_Set.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/Groebner_Basis.thy` (diff)
The file was modified	`src/HOL/Groups.thy` (diff)
The file was modified	`src/HOL/Groups_Big.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/Hilbert_Choice.thy` (diff)
The file was modified	`src/HOL/Inductive.thy` (diff)
The file was modified	`src/HOL/Int.thy` (diff)
The file was modified	`src/HOL/Isar_Examples/Higher_Order_Logic.thy` (diff)
The file was modified	`src/HOL/Lattices.thy` (diff)
The file was modified	`src/HOL/Lattices_Big.thy` (diff)
The file was modified	`src/HOL/Library/AList.thy` (diff)
The file was modified	`src/HOL/Library/Bit.thy` (diff)
The file was modified	`src/HOL/Library/Cancellation/cancel.ML` (diff)
The file was modified	`src/HOL/Library/Cancellation/cancel_data.ML` (diff)
The file was modified	`src/HOL/Library/Cancellation/cancel_simprocs.ML` (diff)
The file was modified	`src/HOL/Library/Cardinality.thy` (diff)
The file was modified	`src/HOL/Library/Code_Abstract_Nat.thy` (diff)
The file was modified	`src/HOL/Library/Code_Binary_Nat.thy` (diff)
The file was modified	`src/HOL/Library/Code_Lazy.thy` (diff)
The file was modified	`src/HOL/Library/Code_Prolog.thy` (diff)
The file was modified	`src/HOL/Library/Code_Target_Nat.thy` (diff)
The file was modified	`src/HOL/Library/Code_Test.thy` (diff)
The file was modified	`src/HOL/Library/Complete_Partial_Order2.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/DAList_Multiset.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_Nat.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Nonnegative_Real.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/Finite_Lattice.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/FuncSet.thy` (diff)
The file was modified	`src/HOL/Library/Function_Division.thy` (diff)
The file was modified	`src/HOL/Library/Going_To_Filter.thy` (diff)
The file was modified	`src/HOL/Library/IArray.thy` (diff)
The file was modified	`src/HOL/Library/Infinite_Set.thy` (diff)
The file was modified	`src/HOL/Library/LaTeXsugar.thy` (diff)
The file was modified	`src/HOL/Library/Lub_Glb.thy` (diff)
The file was modified	`src/HOL/Library/Monad_Syntax.thy` (diff)
The file was modified	`src/HOL/Library/Multiset.thy` (diff)
The file was modified	`src/HOL/Library/Nat_Bijection.thy` (diff)
The file was modified	`src/HOL/Library/Nonpos_Ints.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/Periodic_Fun.thy` (diff)
The file was modified	`src/HOL/Library/Phantom_Type.thy` (diff)
The file was modified	`src/HOL/Library/Predicate_Compile_Alternative_Defs.thy` (diff)
The file was modified	`src/HOL/Library/Quotient_Type.thy` (diff)
The file was modified	`src/HOL/Library/RBT_Impl.thy` (diff)
The file was modified	`src/HOL/Library/RBT_Mapping.thy` (diff)
The file was modified	`src/HOL/Library/Ramsey.thy` (diff)
The file was modified	`src/HOL/Library/Sum_of_Squares/sos_wrapper.ML` (diff)
The file was modified	`src/HOL/Library/Tree.thy` (diff)
The file was modified	`src/HOL/Library/Tree_Multiset.thy` (diff)
The file was modified	`src/HOL/Library/Tree_Real.thy` (diff)
The file was modified	`src/HOL/Library/Type_Length.thy` (diff)
The file was modified	`src/HOL/Library/While_Combinator.thy` (diff)
The file was modified	`src/HOL/Library/adhoc_overloading.ML` (diff)
The file was modified	`src/HOL/Library/case_converter.ML` (diff)
The file was modified	`src/HOL/Library/cconv.ML` (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/Library/conditional_parametricity.ML` (diff)
The file was modified	`src/HOL/Library/datatype_records.ML` (diff)
The file was modified	`src/HOL/Library/multiset_simprocs.ML` (diff)
The file was modified	`src/HOL/Library/old_recdef.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/Library/rewrite.ML` (diff)
The file was modified	`src/HOL/Library/simps_case_conv.ML` (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/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/Num.thy` (diff)
The file was modified	`src/HOL/Numeral_Simprocs.thy` (diff)
The file was modified	`src/HOL/Orderings.thy` (diff)
The file was modified	`src/HOL/Parity.thy` (diff)
The file was modified	`src/HOL/Partial_Function.thy` (diff)
The file was modified	`src/HOL/Power.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile.thy` (diff)
The file was modified	`src/HOL/Presburger.thy` (diff)
The file was modified	`src/HOL/Product_Type.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/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/Rings.thy` (diff)
The file was modified	`src/HOL/Semiring_Normalization.thy` (diff)
The file was modified	`src/HOL/Series.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/TPTP/TPTP_Parser/tptp_syntax.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_satallax.ML` (diff)
The file was modified	`src/HOL/Tools/ATP/atp_systems.ML` (diff)
The file was modified	`src/HOL/Tools/ATP/atp_util.ML` (diff)
The file was modified	`src/HOL/Tools/ATP/atp_waldmeister.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_axiomatization.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_comp.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_def.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_def_sugar_tactics.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_n2m.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_n2m_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_fp_rec_sugar_util.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_grec.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_tactics.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_grec_tactics.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.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_gfp_util.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_compat.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_countable.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_size.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_util.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lift.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_tactics.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_util.ML` (diff)
The file was modified	`src/HOL/Tools/Ctr_Sugar/case_translation.ML` (diff)
The file was modified	`src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML` (diff)
The file was modified	`src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML` (diff)
The file was modified	`src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML` (diff)
The file was modified	`src/HOL/Tools/Function/function_lib.ML` (diff)
The file was modified	`src/HOL/Tools/Function/lexicographic_order.ML` (diff)
The file was modified	`src/HOL/Tools/Function/partial_function.ML` (diff)
The file was modified	`src/HOL/Tools/Function/scnp_reconstruct.ML` (diff)
The file was modified	`src/HOL/Tools/Function/sum_tree.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_bnf.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_def.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_def_code_dt.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_info.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_setup.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_term.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_util.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_generate.ML` (diff)
The file was modified	`src/HOL/Tools/Metis/metis_reconstruct.ML` (diff)
The file was modified	`src/HOL/Tools/Metis/metis_tactic.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_commands.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_hol.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_kodkod.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_nut.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_preproc.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_rep.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_scope.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_tests.ML` (diff)
The file was modified	`src/HOL/Tools/Nitpick/nitpick_util.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_commands.ML` (diff)
The file was modified	`src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML` (diff)
The file was modified	`src/HOL/Tools/Nunchaku/nunchaku_translate.ML` (diff)
The file was modified	`src/HOL/Tools/Nunchaku/nunchaku_util.ML` (diff)
The file was modified	`src/HOL/Tools/Old_Datatype/old_datatype_aux.ML` (diff)
The file was modified	`src/HOL/Tools/Old_Datatype/old_datatype_data.ML` (diff)
The file was modified	`src/HOL/Tools/Old_Datatype/old_datatype_prop.ML` (diff)
The file was modified	`src/HOL/Tools/Old_Datatype/old_primrec.ML` (diff)
The file was modified	`src/HOL/Tools/Old_Datatype/old_rep_datatype.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/mode_inference.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML` (diff)
The file was modified	`src/HOL/Tools/Qelim/cooper.ML` (diff)
The file was modified	`src/HOL/Tools/Qelim/qelim.ML` (diff)
The file was modified	`src/HOL/Tools/Quickcheck/random_generators.ML` (diff)
The file was modified	`src/HOL/Tools/Quotient/quotient_def.ML` (diff)
The file was modified	`src/HOL/Tools/Quotient/quotient_info.ML` (diff)
The file was modified	`src/HOL/Tools/Quotient/quotient_tacs.ML` (diff)
The file was modified	`src/HOL/Tools/Quotient/quotient_term.ML` (diff)
The file was modified	`src/HOL/Tools/Quotient/quotient_type.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/conj_disj_perm.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_normalize.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_real.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_replay.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_replay_methods.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_solver.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_systems.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/verit_replay.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/verit_replay_methods.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/z3_interface.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/z3_isar.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/z3_proof.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/z3_real.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/Sledgehammer/sledgehammer_commands.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_mash.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/Sledgehammer/sledgehammer_prover_minimize.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML` (diff)
The file was modified	`src/HOL/Tools/Transfer/transfer.ML` (diff)
The file was modified	`src/HOL/Tools/Transfer/transfer_bnf.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/hologic.ML` (diff)
The file was modified	`src/HOL/Tools/inductive.ML` (diff)
The file was modified	`src/HOL/Tools/inductive_realizer.ML` (diff)
The file was modified	`src/HOL/Tools/inductive_set.ML` (diff)
The file was modified	`src/HOL/Tools/int_arith.ML` (diff)
The file was modified	`src/HOL/Tools/lambda_lifting.ML` (diff)
The file was modified	`src/HOL/Tools/lin_arith.ML` (diff)
The file was modified	`src/HOL/Tools/literal.ML` (diff)
The file was modified	`src/HOL/Tools/nat_numeral_simprocs.ML` (diff)
The file was modified	`src/HOL/Tools/numeral.ML` (diff)
The file was modified	`src/HOL/Tools/numeral_simprocs.ML` (diff)
The file was modified	`src/HOL/Tools/prop_logic.ML` (diff)
The file was modified	`src/HOL/Tools/record.ML` (diff)
The file was modified	`src/HOL/Tools/reflection.ML` (diff)
The file was modified	`src/HOL/Tools/reification.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/Tools/semiring_normalizer.ML` (diff)
The file was modified	`src/HOL/Tools/set_comprehension_pointfree.ML` (diff)
The file was modified	`src/HOL/Tools/simpdata.ML` (diff)
The file was modified	`src/HOL/Tools/string_syntax.ML` (diff)
The file was modified	`src/HOL/Tools/try0.ML` (diff)
The file was modified	`src/HOL/Topological_Spaces.thy` (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/Typerep.thy` (diff)
The file was modified	`src/HOL/Vector_Spaces.thy` (diff)
The file was modified	`src/HOL/Wellfounded.thy` (diff)
The file was modified	`src/HOL/Wfrec.thy` (diff)
The file was modified	`src/HOL/Zorn.thy` (diff)
The file was modified	`src/Provers/Arith/cancel_div_mod.ML` (diff)
The file was modified	`src/Provers/blast.ML` (diff)
The file was modified	`src/Provers/clasimp.ML` (diff)
The file was modified	`src/Provers/classical.ML` (diff)
The file was modified	`src/Provers/hypsubst.ML` (diff)
The file was modified	`src/Provers/splitter.ML` (diff)
The file was modified	`src/Sequents/ILL.thy` (diff)
The file was modified	`src/Sequents/LK.thy` (diff)
The file was modified	`src/Sequents/LK0.thy` (diff)
The file was modified	`src/Sequents/Modal0.thy` (diff)
The file was modified	`src/Sequents/S43.thy` (diff)
The file was modified	`src/Sequents/Sequents.thy` (diff)
The file was modified	`src/Sequents/modal.ML` (diff)
The file was modified	`src/Sequents/prover.ML` (diff)
The file was modified	`src/Sequents/simpdata.ML` (diff)
The file was modified	`src/Tools/Code/code_haskell.ML` (diff)
The file was modified	`src/Tools/Code/code_preproc.ML` (diff)
The file was modified	`src/Tools/Code/code_printer.ML` (diff)
The file was modified	`src/Tools/Code/code_runtime.ML` (diff)
The file was modified	`src/Tools/Code/code_simp.ML` (diff)
The file was modified	`src/Tools/Code/code_target.ML` (diff)
The file was modified	`src/Tools/Code/code_thingol.ML` (diff)
The file was modified	`src/Tools/Spec_Check/Examples.thy` (diff)
The file was modified	`src/Tools/Spec_Check/spec_check.ML` (diff)
The file was modified	`src/Tools/induct.ML` (diff)
The file was modified	`src/Tools/misc_legacy.ML` (diff)
The file was modified	`src/Tools/nbe.ML` (diff)
The file was modified	`src/Tools/solve_direct.ML` (diff)
The file was modified	`src/Tools/try.ML` (diff)
The file was modified	`src/ZF/Arith.thy` (diff)
The file was modified	`src/ZF/ArithSimp.thy` (diff)
The file was modified	`src/ZF/Bin.thy` (diff)
The file was modified	`src/ZF/Cardinal.thy` (diff)
The file was modified	`src/ZF/CardinalArith.thy` (diff)
The file was modified	`src/ZF/Cardinal_AC.thy` (diff)
The file was modified	`src/ZF/Constructible/AC_in_L.thy` (diff)
The file was modified	`src/ZF/Constructible/DPow_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Datatype_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Formula.thy` (diff)
The file was modified	`src/ZF/Constructible/Internalize.thy` (diff)
The file was modified	`src/ZF/Constructible/L_axioms.thy` (diff)
The file was modified	`src/ZF/Constructible/Normal.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/Constructible/Rec_Separation.thy` (diff)
The file was modified	`src/ZF/Constructible/Reflection.thy` (diff)
The file was modified	`src/ZF/Constructible/Relative.thy` (diff)
The file was modified	`src/ZF/Constructible/Satisfies_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Separation.thy` (diff)
The file was modified	`src/ZF/Constructible/WF_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/WFrec.thy` (diff)
The file was modified	`src/ZF/Constructible/Wellorderings.thy` (diff)
The file was modified	`src/ZF/Datatype.thy` (diff)
The file was modified	`src/ZF/Epsilon.thy` (diff)
The file was modified	`src/ZF/EquivClass.thy` (diff)
The file was modified	`src/ZF/Fixedpt.thy` (diff)
The file was modified	`src/ZF/Induct/Acc.thy` (diff)
The file was modified	`src/ZF/Induct/Binary_Trees.thy` (diff)
The file was modified	`src/ZF/Induct/Comb.thy` (diff)
The file was modified	`src/ZF/Induct/Datatypes.thy` (diff)
The file was modified	`src/ZF/Induct/FoldSet.thy` (diff)
The file was modified	`src/ZF/Induct/Multiset.thy` (diff)
The file was modified	`src/ZF/Induct/Ntree.thy` (diff)
The file was modified	`src/ZF/Induct/Primrec.thy` (diff)
The file was modified	`src/ZF/Induct/PropLog.thy` (diff)
The file was modified	`src/ZF/Induct/Term.thy` (diff)
The file was modified	`src/ZF/Induct/Tree_Forest.thy` (diff)
The file was modified	`src/ZF/Inductive.thy` (diff)
The file was modified	`src/ZF/Int.thy` (diff)
The file was modified	`src/ZF/IntDiv.thy` (diff)
The file was modified	`src/ZF/Nat.thy` (diff)
The file was modified	`src/ZF/OrdQuant.thy` (diff)
The file was modified	`src/ZF/OrderArith.thy` (diff)
The file was modified	`src/ZF/OrderType.thy` (diff)
The file was modified	`src/ZF/Ordinal.thy` (diff)
The file was modified	`src/ZF/Perm.thy` (diff)
The file was modified	`src/ZF/Sum.thy` (diff)
The file was modified	`src/ZF/Tools/cartprod.ML` (diff)
The file was modified	`src/ZF/Tools/datatype_package.ML` (diff)
The file was modified	`src/ZF/Tools/ind_cases.ML` (diff)
The file was modified	`src/ZF/Tools/induct_tacs.ML` (diff)
The file was modified	`src/ZF/Tools/inductive_package.ML` (diff)
The file was modified	`src/ZF/Tools/numeral_syntax.ML` (diff)
The file was modified	`src/ZF/Tools/primrec_package.ML` (diff)
The file was modified	`src/ZF/Tools/typechk.ML` (diff)
The file was modified	`src/ZF/UNITY/AllocBase.thy` (diff)
The file was modified	`src/ZF/UNITY/AllocImpl.thy` (diff)
The file was modified	`src/ZF/UNITY/Constrains.thy` (diff)
The file was modified	`src/ZF/UNITY/SubstAx.thy` (diff)
The file was modified	`src/ZF/UNITY/UNITY.thy` (diff)
The file was modified	`src/ZF/Univ.thy` (diff)
The file was modified	`src/ZF/WF.thy` (diff)
The file was modified	`src/ZF/ZF.thy` (diff)
The file was modified	`src/ZF/ZF_Base.thy` (diff)
The file was modified	`src/ZF/Zorn.thy` (diff)
The file was modified	`src/ZF/arith_data.ML` (diff)
The file was modified	`src/ZF/equalities.thy` (diff)
The file was modified	`src/ZF/ex/CoUnit.thy` (diff)
The file was modified	`src/ZF/ex/Group.thy` (diff)
The file was modified	`src/ZF/ex/Primes.thy` (diff)
The file was modified	`src/ZF/func.thy` (diff)
The file was modified	`src/ZF/ind_syntax.ML` (diff)
The file was modified	`src/ZF/int_arith.ML` (diff)
The file was modified	`src/ZF/pair.thy` (diff)
The file was modified	`src/ZF/simpdata.ML` (diff)
The file was modified	`src/ZF/upair.thy` (diff)
Changeset 69592:a80d8ec6c998 by wenzelm: support for isabelle update -u control_cartouches;
The file was modified	`NEWS` (diff)
The file was modified	`etc/options` (diff)
The file was modified	`src/HOL/Library/LaTeXsugar.thy` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_util.ML` (diff)
The file was modified	`src/HOL/Tools/value_command.ML` (diff)
The file was modified	`src/Pure/General/antiquote.ML` (diff)
The file was modified	`src/Pure/General/symbol.ML` (diff)
The file was modified	`src/Pure/ML/ml_antiquotation.ML` (diff)
The file was modified	`src/Pure/ML/ml_antiquotations.ML` (diff)
The file was modified	`src/Pure/ML/ml_context.ML` (diff)
The file was modified	`src/Pure/PIDE/resources.ML` (diff)
The file was modified	`src/Pure/Thy/document_antiquotation.ML` (diff)
The file was modified	`src/Pure/Thy/document_antiquotations.ML` (diff)
The file was modified	`src/Pure/Thy/thy_output.ML` (diff)
The file was modified	`src/Pure/Tools/jedit.ML` (diff)
The file was modified	`src/Pure/Tools/named_theorems.ML` (diff)
The file was modified	`src/Pure/Tools/plugin.ML` (diff)
The file was modified	`src/Pure/Tools/rail.ML` (diff)
The file was modified	`src/Pure/simplifier.ML` (diff)