Changes

Summary

tuned proofs, to allow unfold_abs_def;
clarified "unfold" operations;
tuned proof;

Changeset 63170:eae6549dbea2 by wenzelm: tuned proofs, to allow unfold_abs_def;
The file was modified	`src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Approximation.thy` (diff)
The file was modified	`src/HOL/Deriv.thy` (diff)
The file was modified	`src/HOL/Inequalities.thy` (diff)
The file was modified	`src/HOL/Library/Complete_Partial_Order2.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/Multivariate_Analysis/Convex_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Multivariate_Analysis/Derivative.thy` (diff)
The file was modified	`src/HOL/Multivariate_Analysis/Determinants.thy` (diff)
The file was modified	`src/HOL/Multivariate_Analysis/Integration.thy` (diff)
The file was modified	`src/HOL/Multivariate_Analysis/Linear_Algebra.thy` (diff)
The file was modified	`src/HOL/Multivariate_Analysis/Polytope.thy` (diff)
The file was modified	`src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy` (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_tactics.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_tactics.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_basic_sugar.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_size.ML` (diff)
The file was modified	`src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML` (diff)
The file was modified	`src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML` (diff)
The file was modified	`src/HOL/Tools/Function/mutual.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/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_setup.ML` (diff)
The file was modified	`src/HOL/Tools/Metis/metis_reconstruct.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_data.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/z3_replay_methods.ML` (diff)
The file was modified	`src/HOL/Tools/Transfer/transfer_bnf.ML` (diff)
The file was modified	`src/HOL/Tools/reification.ML` (diff)
The file was modified	`src/HOL/Topological_Spaces.thy` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)
Changeset 63169:d36c7dc40000 by wenzelm: clarified "unfold" operations;
The file was modified	`src/Pure/Isar/local_defs.ML` (diff)
Changeset 63168:466177e5736c by wenzelm: tuned proof;
The file was modified	`src/ZF/OrderType.thy` (diff)