Simplifier already setup in Pure;
authorwenzelm
Sun May 22 16:51:07 2005 +0200 (2005-05-22)
changeset 160190e1405402d53
parent 16018 3e4e077af2e7
child 16020 ace2c610b5be
Simplifier already setup in Pure;
doc-src/Ref/simplifier.tex
src/FOL/IFOL.thy
src/FOL/IsaMakefile
src/FOL/ROOT.ML
src/FOL/simpdata.ML
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/ROOT.ML
src/Provers/README
src/Provers/clasimp.ML
src/Sequents/LK0.thy
src/Sequents/ROOT.ML
     1.1 --- a/doc-src/Ref/simplifier.tex	Sun May 22 16:51:06 2005 +0200
     1.2 +++ b/doc-src/Ref/simplifier.tex	Sun May 22 16:51:07 2005 +0200
     1.3 @@ -1224,12 +1224,10 @@
     1.4  first-order logic; the code is largely taken from {\tt FOL/simpdata.ML} of the
     1.5  Isabelle sources.
     1.6  
     1.7 -The simplifier and the case splitting tactic, which reside on separate files,
     1.8 -are not part of Pure Isabelle.  They must be loaded explicitly by the
     1.9 -object-logic as follows (below \texttt{\~\relax\~\relax} refers to
    1.10 -\texttt{\$ISABELLE_HOME}):
    1.11 +The case splitting tactic, which resides on a separate files, is not part of
    1.12 +Pure Isabelle.  It needs to be loaded explicitly by the object-logic as
    1.13 +follows (below \texttt{\~\relax\~\relax} refers to \texttt{\$ISABELLE_HOME}):
    1.14  \begin{ttbox}
    1.15 -use "\~\relax\~\relax/src/Provers/simplifier.ML";
    1.16  use "\~\relax\~\relax/src/Provers/splitter.ML";
    1.17  \end{ttbox}
    1.18  
    1.19 @@ -1461,23 +1459,6 @@
    1.20  \end{ttbox}
    1.21  
    1.22  
    1.23 -\subsection{Theory setup}\index{simplification!setting up the theory}
    1.24 -\begin{ttbox}\indexbold{*Simplifier.setup}\index{*setup!simplifier}
    1.25 -Simplifier.setup: (theory -> theory) list
    1.26 -\end{ttbox}
    1.27 -
    1.28 -Advanced theory related features of the simplifier (e.g.\ implicit
    1.29 -simpset support) have to be set up explicitly.  The simplifier already
    1.30 -provides a suitable setup function definition.  This has to be
    1.31 -installed into the base theory of any new object-logic via a
    1.32 -\texttt{setup} declaration.
    1.33 -
    1.34 -For example, this is done in \texttt{FOL/IFOL.thy} as follows:
    1.35 -\begin{ttbox}
    1.36 -setup Simplifier.setup
    1.37 -\end{ttbox}
    1.38 -
    1.39 -
    1.40  \index{simplification|)}
    1.41  
    1.42  
     2.1 --- a/src/FOL/IFOL.thy	Sun May 22 16:51:06 2005 +0200
     2.2 +++ b/src/FOL/IFOL.thy	Sun May 22 16:51:07 2005 +0200
     2.3 @@ -140,7 +140,6 @@
     2.4  
     2.5  subsection {* Lemmas and proof tools *}
     2.6  
     2.7 -setup Simplifier.setup
     2.8  use "IFOL_lemmas.ML"
     2.9  
    2.10  use "fologic.ML"
     3.1 --- a/src/FOL/IsaMakefile	Sun May 22 16:51:06 2005 +0200
     3.2 +++ b/src/FOL/IsaMakefile	Sun May 22 16:51:07 2005 +0200
     3.3 @@ -28,15 +28,15 @@
     3.4  
     3.5  $(OUT)/Pure: Pure
     3.6  
     3.7 -$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML	$(SRC)/Provers/make_elim.ML \
     3.8 -  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
     3.9 -  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \
    3.10 -  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/quantifier1.ML\
    3.11 -  $(SRC)/Provers/eqsubst.ML\
    3.12 -  eqrule_FOL_data.ML\
    3.13 -  FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML IFOL.thy \
    3.14 -  IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML document/root.tex \
    3.15 -  fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
    3.16 +$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML				\
    3.17 +  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
    3.18 +  $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
    3.19 +  $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML			\
    3.20 +  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/quantifier1.ML		\
    3.21 +  $(SRC)/Provers/splitter.ML FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML	\
    3.22 +  IFOL.thy IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML		\
    3.23 +  document/root.tex eqrule_FOL_data.ML fologic.ML hypsubstdata.ML	\
    3.24 +  intprover.ML simpdata.ML
    3.25  	@$(ISATOOL) usedir -b $(OUT)/Pure FOL
    3.26  
    3.27  
     4.1 --- a/src/FOL/ROOT.ML	Sun May 22 16:51:06 2005 +0200
     4.2 +++ b/src/FOL/ROOT.ML	Sun May 22 16:51:07 2005 +0200
     4.3 @@ -10,7 +10,6 @@
     4.4  
     4.5  print_depth 1;  
     4.6  
     4.7 -use "~~/src/Provers/simplifier.ML";
     4.8  use "~~/src/Provers/splitter.ML";
     4.9  use "~~/src/Provers/ind.ML";
    4.10  use "~~/src/Provers/hypsubst.ML";
     5.1 --- a/src/FOL/simpdata.ML	Sun May 22 16:51:06 2005 +0200
     5.2 +++ b/src/FOL/simpdata.ML	Sun May 22 16:51:07 2005 +0200
     5.3 @@ -105,10 +105,10 @@
     5.4    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
     5.5     ("All", [spec]), ("True", []), ("False", [])];
     5.6  
     5.7 -(* ###FIXME: move to Provers/simplifier.ML
     5.8 +(* ###FIXME: move to simplifier.ML
     5.9  val mk_atomize:      (string * thm list) list -> thm -> thm list
    5.10  *)
    5.11 -(* ###FIXME: move to Provers/simplifier.ML *)
    5.12 +(* ###FIXME: move to simplifier.ML *)
    5.13  fun mk_atomize pairs =
    5.14    let fun atoms th =
    5.15          (case concl_of th of
     6.1 --- a/src/HOL/HOL.thy	Sun May 22 16:51:06 2005 +0200
     6.2 +++ b/src/HOL/HOL.thy	Sun May 22 16:51:07 2005 +0200
     6.3 @@ -1124,7 +1124,6 @@
     6.4  subsubsection {* Actual Installation of the Simplifier *}
     6.5  
     6.6  use "simpdata.ML"
     6.7 -setup Simplifier.setup
     6.8  setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
     6.9  setup Splitter.setup setup Clasimp.setup
    6.10  
     7.1 --- a/src/HOL/IsaMakefile	Sun May 22 16:51:06 2005 +0200
     7.2 +++ b/src/HOL/IsaMakefile	Sun May 22 16:51:07 2005 +0200
     7.3 @@ -61,64 +61,59 @@
     7.4  Pure:
     7.5  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     7.6  
     7.7 -$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/quantifier1.ML \
     7.8 -  $(SRC)/Provers/Arith/abel_cancel.ML \
     7.9 -  $(SRC)/Provers/Arith/assoc_fold.ML \
    7.10 -  $(SRC)/Provers/Arith/cancel_numerals.ML \
    7.11 -  $(SRC)/Provers/Arith/cancel_sums.ML \
    7.12 -  $(SRC)/Provers/Arith/combine_numerals.ML \
    7.13 -  $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
    7.14 -  $(SRC)/Provers/Arith/extract_common_term.ML \
    7.15 -  $(SRC)/Provers/Arith/cancel_div_mod.ML \
    7.16 -  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
    7.17 -  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    7.18 -  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
    7.19 -  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/order.ML $(SRC)/Provers/quasi.ML\
    7.20 -  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
    7.21 -  $(SRC)/Provers/trancl.ML \
    7.22 -  $(SRC)/TFL/casesplit.ML \
    7.23 -  $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
    7.24 -  $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
    7.25 -  $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
    7.26 -  $(SRC)/Provers/eqsubst.ML\
    7.27 -  eqrule_HOL_data.ML\
    7.28 -  Datatype.ML Datatype.thy Datatype_Universe.thy \
    7.29 -  Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
    7.30 -  Fun.thy Gfp.thy Hilbert_Choice.thy HOL.ML \
    7.31 -  HOL.thy Inductive.thy Infinite_Set.thy Integ/Numeral.thy \
    7.32 -  Integ/cooper_dec.ML Integ/cooper_proof.ML \
    7.33 -  Integ/IntArith.thy Integ/IntDef.thy \
    7.34 -  Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \
    7.35 -  Integ/int_arith1.ML Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
    7.36 -  Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
    7.37 -  Lattice_Locales.thy Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy\
    7.38 -  Nat.ML Nat.thy NatArith.thy Power.thy PreList.thy Product_Type.thy \
    7.39 -  Refute.thy ROOT.ML \
    7.40 -  Recdef.thy Reconstruction.thy Record.thy Relation.ML Relation.thy \
    7.41 -  Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML \
    7.42 -  Orderings.ML Orderings.thy Ring_and_Field.thy\
    7.43 -  Set.ML Set.thy SetInterval.thy \
    7.44 -  Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
    7.45 - Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
    7.46 - Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \
    7.47 - Tools/inductive_codegen.ML Tools/inductive_package.ML Tools/inductive_realizer.ML \
    7.48 - Tools/meson.ML Tools/numeral_syntax.ML \
    7.49 - Tools/primrec_package.ML Tools/prop_logic.ML \
    7.50 - Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \
    7.51 - Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \
    7.52 - Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \
    7.53 - Tools/split_rule.ML Tools/typedef_package.ML \
    7.54 -  Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
    7.55 -  Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \
    7.56 -  blastdata.ML cladata.ML \
    7.57 - Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
    7.58 - Tools/res_axioms.ML Tools/res_types_sorts.ML \
    7.59 - Tools/ATP/recon_prelim.ML Tools/ATP/recon_order_clauses.ML\
    7.60 - Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML \
    7.61 - Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \
    7.62 - Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML  \
    7.63 - Tools/ATP/watcher.sig Tools/ATP/watcher.ML   Tools/res_atp.ML\
    7.64 - document/root.tex hologic.ML simpdata.ML thy_syntax.ML
    7.65 +$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML			\
    7.66 +  $(SRC)/Provers/Arith/assoc_fold.ML						\
    7.67 +  $(SRC)/Provers/Arith/cancel_div_mod.ML					\
    7.68 +  $(SRC)/Provers/Arith/cancel_numeral_factor.ML					\
    7.69 +  $(SRC)/Provers/Arith/cancel_numerals.ML					\
    7.70 +  $(SRC)/Provers/Arith/cancel_sums.ML						\
    7.71 +  $(SRC)/Provers/Arith/combine_numerals.ML					\
    7.72 +  $(SRC)/Provers/Arith/extract_common_term.ML					\
    7.73 +  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML		\
    7.74 +  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML				\
    7.75 +  $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML				\
    7.76 +  $(SRC)/Provers/induct_method.ML $(SRC)/Provers/make_elim.ML			\
    7.77 +  $(SRC)/Provers/order.ML $(SRC)/Provers/quantifier1.ML				\
    7.78 +  $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/trancl.ML	\
    7.79 +  $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML		\
    7.80 +  $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML			\
    7.81 +  $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML			\
    7.82 +  Datatype.ML Datatype.thy Datatype_Universe.thy Divides.thy			\
    7.83 +  Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy		\
    7.84 +  Fun.thy Gfp.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy		\
    7.85 +  Infinite_Set.thy Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy		\
    7.86 +  Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Numeral.thy			\
    7.87 +  Integ/Parity.thy Integ/Presburger.thy Integ/cooper_dec.ML			\
    7.88 +  Integ/cooper_proof.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML	\
    7.89 +  Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy		\
    7.90 +  Lattice_Locales.thy Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy		\
    7.91 +  Nat.ML Nat.thy NatArith.thy OrderedGroup.ML OrderedGroup.thy			\
    7.92 +  Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
    7.93 +  ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
    7.94 +  Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML		\
    7.95 +  Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/SpassCommunication.ML		\
    7.96 +  Tools/ATP/VampireCommunication.ML Tools/ATP/modUnix.ML			\
    7.97 +  Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML			\
    7.98 +  Tools/ATP/recon_prelim.ML Tools/ATP/recon_transfer_proof.ML			\
    7.99 +  Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML		\
   7.100 +  Tools/ATP/watcher.ML Tools/ATP/watcher.sig					\
   7.101 +  Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML				\
   7.102 +  Tools/datatype_codegen.ML Tools/datatype_package.ML				\
   7.103 +  Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
   7.104 +  Tools/datatype_rep_proofs.ML Tools/inductive_codegen.ML			\
   7.105 +  Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML		\
   7.106 +  Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/prop_logic.ML		\
   7.107 +  Tools/recdef_package.ML Tools/recfun_codegen.ML				\
   7.108 +  Tools/reconstruction.ML Tools/record_package.ML Tools/refute.ML		\
   7.109 +  Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML			\
   7.110 +  Tools/res_clause.ML Tools/res_lib.ML Tools/res_skolem_function.ML		\
   7.111 +  Tools/res_types_sorts.ML Tools/rewrite_hol_proof.ML				\
   7.112 +  Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML	\
   7.113 +  Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy		\
   7.114 +  Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy		\
   7.115 +  antisym_setup.ML arith_data.ML blastdata.ML cladata.ML			\
   7.116 +  document/root.tex eqrule_HOL_data.ML hologic.ML simpdata.ML			\
   7.117 +  thy_syntax.ML
   7.118  	@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
   7.119  
   7.120  
   7.121 @@ -126,14 +121,15 @@
   7.122  
   7.123  HOL-Complex-HahnBanach: HOL-Complex $(LOG)/HOL-Complex-HahnBanach.gz
   7.124  
   7.125 -$(LOG)/HOL-Complex-HahnBanach.gz: $(OUT)/HOL-Complex Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
   7.126 -  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
   7.127 -  Real/HahnBanach/HahnBanachExtLemmas.thy	\
   7.128 -  Real/HahnBanach/HahnBanachSupLemmas.thy	\
   7.129 -  Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
   7.130 -  Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
   7.131 -  Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
   7.132 -  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \
   7.133 +$(LOG)/HOL-Complex-HahnBanach.gz: $(OUT)/HOL-Complex			\
   7.134 +  Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy		\
   7.135 +  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy	\
   7.136 +  Real/HahnBanach/HahnBanachExtLemmas.thy				\
   7.137 +  Real/HahnBanach/HahnBanachSupLemmas.thy				\
   7.138 +  Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy	\
   7.139 +  Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML			\
   7.140 +  Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy		\
   7.141 +  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib	\
   7.142    Real/HahnBanach/document/root.tex
   7.143  	@cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL-Complex HahnBanach
   7.144  
   7.145 @@ -142,24 +138,23 @@
   7.146  
   7.147  HOL-Complex: HOL $(OUT)/HOL-Complex
   7.148  
   7.149 -$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML\
   7.150 -  Library/Zorn.thy\
   7.151 -  Real/Lubs.thy Real/rat_arith.ML\
   7.152 -  Real/Rational.thy Real/PReal.thy Real/RComplete.thy \
   7.153 -  Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy \
   7.154 -  Real/RealPow.thy Real/document/root.tex\
   7.155 -  Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy\
   7.156 -  Hyperreal/Filter.thy Hyperreal/HSeries.thy\
   7.157 -  Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\
   7.158 -  Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
   7.159 -  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
   7.160 -  Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy\
   7.161 -  Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\
   7.162 -  Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy\
   7.163 -  Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy \
   7.164 -  Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
   7.165 -  Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy\
   7.166 -  Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy\
   7.167 +$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML Library/Zorn.thy			\
   7.168 +  Real/Lubs.thy Real/rat_arith.ML						\
   7.169 +  Real/Rational.thy Real/PReal.thy Real/RComplete.thy				\
   7.170 +  Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy		\
   7.171 +  Real/RealPow.thy Real/document/root.tex					\
   7.172 +  Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy			\
   7.173 +  Hyperreal/Filter.thy Hyperreal/HSeries.thy					\
   7.174 +  Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy			\
   7.175 +  Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy					\
   7.176 +  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy				\
   7.177 +  Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy			\
   7.178 +  Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy					\
   7.179 +  Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy			\
   7.180 +  Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy			\
   7.181 +  Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML	\
   7.182 +  Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy			\
   7.183 +  Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy			\
   7.184    Complex/NSCA.thy Complex/NSComplex.thy Complex/document/root.tex 
   7.185  	@cd Complex; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Complex
   7.186  
     8.1 --- a/src/HOL/ROOT.ML	Sun May 22 16:51:06 2005 +0200
     8.2 +++ b/src/HOL/ROOT.ML	Sun May 22 16:51:07 2005 +0200
     8.3 @@ -16,7 +16,6 @@
     8.4  
     8.5  use "hologic.ML";
     8.6  
     8.7 -use "~~/src/Provers/simplifier.ML";
     8.8  use "~~/src/Provers/splitter.ML";
     8.9  use "~~/src/Provers/hypsubst.ML";
    8.10  use "~~/src/Provers/induct_method.ML";
     9.1 --- a/src/Provers/README	Sun May 22 16:51:06 2005 +0200
     9.2 +++ b/src/Provers/README	Sun May 22 16:51:07 2005 +0200
     9.3 @@ -14,9 +14,8 @@
     9.4    linorder.ML		transitivity reasoner for linear (total) orders
     9.5    quantifier1.ML	simplification procedures for "1 point rules"
     9.6    simp.ML               powerful but slow simplifier
     9.7 -  simplifier.ML         fast simplifier
     9.8    split_paired_all.ML	turn surjective pairing into split rule
     9.9 -  splitter.ML           performs case splits for simplifier.ML
    9.10 +  splitter.ML           performs case splits for simplifier
    9.11    typedsimp.ML          basic simplifier for explicitly typed logics
    9.12  
    9.13  directory Arith:
    10.1 --- a/src/Provers/clasimp.ML	Sun May 22 16:51:06 2005 +0200
    10.2 +++ b/src/Provers/clasimp.ML	Sun May 22 16:51:07 2005 +0200
    10.3 @@ -3,7 +3,7 @@
    10.4      Author:     David von Oheimb, TU Muenchen
    10.5  
    10.6  Combination of classical reasoner and simplifier (depends on
    10.7 -simplifier.ML, splitter.ML classical.ML, blast.ML).
    10.8 +splitter.ML, classical.ML, blast.ML).
    10.9  *)
   10.10  
   10.11  infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2
    11.1 --- a/src/Sequents/LK0.thy	Sun May 22 16:51:06 2005 +0200
    11.2 +++ b/src/Sequents/LK0.thy	Sun May 22 16:51:07 2005 +0200
    11.3 @@ -123,10 +123,6 @@
    11.4    If :: [o, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
    11.5     "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
    11.6  
    11.7 -
    11.8 -setup
    11.9 -  Simplifier.setup
   11.10 -
   11.11  setup
   11.12    prover_setup
   11.13  
    12.1 --- a/src/Sequents/ROOT.ML	Sun May 22 16:51:06 2005 +0200
    12.2 +++ b/src/Sequents/ROOT.ML	Sun May 22 16:51:07 2005 +0200
    12.3 @@ -14,8 +14,6 @@
    12.4  Unify.trace_bound:= 20;
    12.5  Unify.search_bound := 40;
    12.6  
    12.7 -use "~~/src/Provers/simplifier.ML";
    12.8 -
    12.9  use_thy "Sequents";
   12.10  use "prover.ML";
   12.11