2005-10-17 wenzelm [Mon, 17 Oct 2005 23:10:22 +0200] rev 17884
moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy;
change_simpset;
src/ZF/Main.thy

2005-10-17 wenzelm [Mon, 17 Oct 2005 23:10:21 +0200] rev 17883
removed obsolete/experimental context components (superceded by Simplifier.the_context);
more abstract change_simpset(_of);
tuned;
src/Pure/simplifier.ML

2005-10-17 wenzelm [Mon, 17 Oct 2005 23:10:20 +0200] rev 17882
added set/addloop' for simpset dependent loopers;
simpset: added context field with the_context, set_context;
added inherit_context (inherits bounds as well);
removed obsolete inherit_bounds;
src/Pure/meta_simplifier.ML

2005-10-17 wenzelm [Mon, 17 Oct 2005 23:10:19 +0200] rev 17881
functor: no Simplifier argument;
change_simpset;
src/Provers/splitter.ML

2005-10-17 wenzelm [Mon, 17 Oct 2005 23:10:18 +0200] rev 17880
change_claset(_of): more abtract interface;
claset_of: init proof context;
added raw get_claset;
src/Provers/classical.ML

2005-10-17 wenzelm [Mon, 17 Oct 2005 23:10:17 +0200] rev 17879
functor: no Simplifier argument;
export change_clasimpset;
src/Provers/clasimp.ML

2005-10-17 wenzelm [Mon, 17 Oct 2005 23:10:16 +0200] rev 17878
tuned;
NEWS src/LCF/ex/Ex1.ML src/LCF/ex/Ex2.ML src/LCF/ex/Ex3.ML src/LCF/ex/Ex4.ML

2005-10-17 wenzelm [Mon, 17 Oct 2005 23:10:15 +0200] rev 17877
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
src/HOL/Algebra/abstract/Ring.thy src/HOL/Fun.thy src/HOL/Integ/int_factor_simprocs.ML src/HOL/Integ/nat_simprocs.ML src/HOL/List.thy src/Provers/Arith/abel_cancel.ML src/Provers/Arith/assoc_fold.ML src/Provers/Arith/fast_lin_arith.ML src/ZF/Datatype.ML src/ZF/Integ/int_arith.ML src/ZF/arith_data.ML

2005-10-17 wenzelm [Mon, 17 Oct 2005 23:10:13 +0200] rev 17876
change_claset/simpset;
src/FOL/cladata.ML src/HOL/Bali/AxSem.thy src/HOL/Bali/Basis.thy src/HOL/Bali/DefiniteAssignment.thy src/HOL/Bali/Eval.thy src/HOL/Bali/Evaln.thy src/HOL/Bali/TypeSafe.thy src/HOL/Bali/WellForm.thy src/HOL/Bali/WellType.thy src/HOL/Datatype.thy src/HOL/Hyperreal/hypreal_arith.ML src/HOL/Library/word_setup.ML src/HOL/MicroJava/Comp/CorrComp.thy src/HOL/Orderings.thy src/HOL/Real/rat_arith.ML src/HOL/Real/real_arith.ML src/HOL/Transitive_Closure.thy src/HOL/antisym_setup.ML src/HOL/cladata.ML src/HOLCF/HOLCF.thy src/HOLCF/IOA/NTP/Correctness.ML src/HOLCF/IOA/meta_theory/CompoTraces.ML src/HOLCF/IOA/meta_theory/TLS.ML src/HOLCF/IOA/meta_theory/Traces.ML src/HOLCF/cont_proc.ML src/LCF/LCF_lemmas.ML src/Sequents/simpdata.ML src/ZF/Main.ML src/ZF/OrdQuant.thy src/ZF/simpdata.ML

2005-10-17 wenzelm [Mon, 17 Oct 2005 23:10:10 +0200] rev 17875
change_claset/simpset;
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
src/FOL/simpdata.ML src/HOL/Integ/int_arith1.ML src/HOL/Product_Type.thy src/HOL/Set.thy src/HOL/Tools/datatype_package.ML src/HOL/Tools/record_package.ML src/HOL/arith_data.ML src/HOL/simpdata.ML