Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simplifier already setup in Pure;
authorwenzelm
Sun, 22 May 2005 16:51:07 +0200
changeset 16019 0e1405402d53
parent 16018 3e4e077af2e7
child 16020 ace2c610b5be
Simplifier already setup in Pure;
doc-src/Ref/simplifier.tex file | annotate | diff | comparison | revisions
src/FOL/IFOL.thy file | annotate | diff | comparison | revisions
src/FOL/IsaMakefile file | annotate | diff | comparison | revisions
src/FOL/ROOT.ML file | annotate | diff | comparison | revisions
src/FOL/simpdata.ML file | annotate | diff | comparison | revisions
src/HOL/HOL.thy file | annotate | diff | comparison | revisions
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOL/ROOT.ML file | annotate | diff | comparison | revisions
src/Provers/README file | annotate | diff | comparison | revisions
src/Provers/clasimp.ML file | annotate | diff | comparison | revisions
src/Sequents/LK0.thy file | annotate | diff | comparison | revisions
src/Sequents/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/doc-src/Ref/simplifier.tex	Sun May 22 16:51:06 2005 +0200
+++ b/doc-src/Ref/simplifier.tex	Sun May 22 16:51:07 2005 +0200
@@ -1224,12 +1224,10 @@
 first-order logic; the code is largely taken from {\tt FOL/simpdata.ML} of the
 Isabelle sources.
 
-The simplifier and the case splitting tactic, which reside on separate files,
-are not part of Pure Isabelle.  They must be loaded explicitly by the
-object-logic as follows (below \texttt{\~\relax\~\relax} refers to
-\texttt{\$ISABELLE_HOME}):
+The case splitting tactic, which resides on a separate files, is not part of
+Pure Isabelle.  It needs to be loaded explicitly by the object-logic as
+follows (below \texttt{\~\relax\~\relax} refers to \texttt{\$ISABELLE_HOME}):
 \begin{ttbox}
-use "\~\relax\~\relax/src/Provers/simplifier.ML";
 use "\~\relax\~\relax/src/Provers/splitter.ML";
 \end{ttbox}
 
@@ -1461,23 +1459,6 @@
 \end{ttbox}
 
 
-\subsection{Theory setup}\index{simplification!setting up the theory}
-\begin{ttbox}\indexbold{*Simplifier.setup}\index{*setup!simplifier}
-Simplifier.setup: (theory -> theory) list
-\end{ttbox}
-
-Advanced theory related features of the simplifier (e.g.\ implicit
-simpset support) have to be set up explicitly.  The simplifier already
-provides a suitable setup function definition.  This has to be
-installed into the base theory of any new object-logic via a
-\texttt{setup} declaration.
-
-For example, this is done in \texttt{FOL/IFOL.thy} as follows:
-\begin{ttbox}
-setup Simplifier.setup
-\end{ttbox}
-
-
 \index{simplification|)}
 
 
--- a/src/FOL/IFOL.thy	Sun May 22 16:51:06 2005 +0200
+++ b/src/FOL/IFOL.thy	Sun May 22 16:51:07 2005 +0200
@@ -140,7 +140,6 @@
 
 subsection {* Lemmas and proof tools *}
 
-setup Simplifier.setup
 use "IFOL_lemmas.ML"
 
 use "fologic.ML"
--- a/src/FOL/IsaMakefile	Sun May 22 16:51:06 2005 +0200
+++ b/src/FOL/IsaMakefile	Sun May 22 16:51:07 2005 +0200
@@ -28,15 +28,15 @@
 
 $(OUT)/Pure: Pure
 
-$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML	$(SRC)/Provers/make_elim.ML \
-  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
-  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \
-  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/quantifier1.ML\
-  $(SRC)/Provers/eqsubst.ML\
-  eqrule_FOL_data.ML\
-  FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML IFOL.thy \
-  IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML document/root.tex \
-  fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
+$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML				\
+  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
+  $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
+  $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML			\
+  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/quantifier1.ML		\
+  $(SRC)/Provers/splitter.ML FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML	\
+  IFOL.thy IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML		\
+  document/root.tex eqrule_FOL_data.ML fologic.ML hypsubstdata.ML	\
+  intprover.ML simpdata.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure FOL
 
 
--- a/src/FOL/ROOT.ML	Sun May 22 16:51:06 2005 +0200
+++ b/src/FOL/ROOT.ML	Sun May 22 16:51:07 2005 +0200
@@ -10,7 +10,6 @@
 
 print_depth 1;  
 
-use "~~/src/Provers/simplifier.ML";
 use "~~/src/Provers/splitter.ML";
 use "~~/src/Provers/ind.ML";
 use "~~/src/Provers/hypsubst.ML";
--- a/src/FOL/simpdata.ML	Sun May 22 16:51:06 2005 +0200
+++ b/src/FOL/simpdata.ML	Sun May 22 16:51:07 2005 +0200
@@ -105,10 +105,10 @@
   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    ("All", [spec]), ("True", []), ("False", [])];
 
-(* ###FIXME: move to Provers/simplifier.ML
+(* ###FIXME: move to simplifier.ML
 val mk_atomize:      (string * thm list) list -> thm -> thm list
 *)
-(* ###FIXME: move to Provers/simplifier.ML *)
+(* ###FIXME: move to simplifier.ML *)
 fun mk_atomize pairs =
   let fun atoms th =
         (case concl_of th of
--- a/src/HOL/HOL.thy	Sun May 22 16:51:06 2005 +0200
+++ b/src/HOL/HOL.thy	Sun May 22 16:51:07 2005 +0200
@@ -1124,7 +1124,6 @@
 subsubsection {* Actual Installation of the Simplifier *}
 
 use "simpdata.ML"
-setup Simplifier.setup
 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
 setup Splitter.setup setup Clasimp.setup
 
--- a/src/HOL/IsaMakefile	Sun May 22 16:51:06 2005 +0200
+++ b/src/HOL/IsaMakefile	Sun May 22 16:51:07 2005 +0200
@@ -61,64 +61,59 @@
 Pure:
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
-$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/quantifier1.ML \
-  $(SRC)/Provers/Arith/abel_cancel.ML \
-  $(SRC)/Provers/Arith/assoc_fold.ML \
-  $(SRC)/Provers/Arith/cancel_numerals.ML \
-  $(SRC)/Provers/Arith/cancel_sums.ML \
-  $(SRC)/Provers/Arith/combine_numerals.ML \
-  $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
-  $(SRC)/Provers/Arith/extract_common_term.ML \
-  $(SRC)/Provers/Arith/cancel_div_mod.ML \
-  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
-  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
-  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
-  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/order.ML $(SRC)/Provers/quasi.ML\
-  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
-  $(SRC)/Provers/trancl.ML \
-  $(SRC)/TFL/casesplit.ML \
-  $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
-  $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
-  $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
-  $(SRC)/Provers/eqsubst.ML\
-  eqrule_HOL_data.ML\
-  Datatype.ML Datatype.thy Datatype_Universe.thy \
-  Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
-  Fun.thy Gfp.thy Hilbert_Choice.thy HOL.ML \
-  HOL.thy Inductive.thy Infinite_Set.thy Integ/Numeral.thy \
-  Integ/cooper_dec.ML Integ/cooper_proof.ML \
-  Integ/IntArith.thy Integ/IntDef.thy \
-  Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \
-  Integ/int_arith1.ML Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
-  Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
-  Lattice_Locales.thy Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy\
-  Nat.ML Nat.thy NatArith.thy Power.thy PreList.thy Product_Type.thy \
-  Refute.thy ROOT.ML \
-  Recdef.thy Reconstruction.thy Record.thy Relation.ML Relation.thy \
-  Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML \
-  Orderings.ML Orderings.thy Ring_and_Field.thy\
-  Set.ML Set.thy SetInterval.thy \
-  Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
- Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
- Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \
- Tools/inductive_codegen.ML Tools/inductive_package.ML Tools/inductive_realizer.ML \
- Tools/meson.ML Tools/numeral_syntax.ML \
- Tools/primrec_package.ML Tools/prop_logic.ML \
- Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \
- Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \
- Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \
- Tools/split_rule.ML Tools/typedef_package.ML \
-  Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
-  Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \
-  blastdata.ML cladata.ML \
- Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
- Tools/res_axioms.ML Tools/res_types_sorts.ML \
- Tools/ATP/recon_prelim.ML Tools/ATP/recon_order_clauses.ML\
- Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML \
- Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \
- Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML  \
- Tools/ATP/watcher.sig Tools/ATP/watcher.ML   Tools/res_atp.ML\
- document/root.tex hologic.ML simpdata.ML thy_syntax.ML
+$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML			\
+  $(SRC)/Provers/Arith/assoc_fold.ML						\
+  $(SRC)/Provers/Arith/cancel_div_mod.ML					\
+  $(SRC)/Provers/Arith/cancel_numeral_factor.ML					\
+  $(SRC)/Provers/Arith/cancel_numerals.ML					\
+  $(SRC)/Provers/Arith/cancel_sums.ML						\
+  $(SRC)/Provers/Arith/combine_numerals.ML					\
+  $(SRC)/Provers/Arith/extract_common_term.ML					\
+  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML		\
+  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML				\
+  $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML				\
+  $(SRC)/Provers/induct_method.ML $(SRC)/Provers/make_elim.ML			\
+  $(SRC)/Provers/order.ML $(SRC)/Provers/quantifier1.ML				\
+  $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/trancl.ML	\
+  $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML		\
+  $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML			\
+  $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML			\
+  Datatype.ML Datatype.thy Datatype_Universe.thy Divides.thy			\
+  Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy		\
+  Fun.thy Gfp.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy		\
+  Infinite_Set.thy Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy		\
+  Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Numeral.thy			\
+  Integ/Parity.thy Integ/Presburger.thy Integ/cooper_dec.ML			\
+  Integ/cooper_proof.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML	\
+  Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy		\
+  Lattice_Locales.thy Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy		\
+  Nat.ML Nat.thy NatArith.thy OrderedGroup.ML OrderedGroup.thy			\
+  Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
+  ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
+  Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML		\
+  Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/SpassCommunication.ML		\
+  Tools/ATP/VampireCommunication.ML Tools/ATP/modUnix.ML			\
+  Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML			\
+  Tools/ATP/recon_prelim.ML Tools/ATP/recon_transfer_proof.ML			\
+  Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML		\
+  Tools/ATP/watcher.ML Tools/ATP/watcher.sig					\
+  Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML				\
+  Tools/datatype_codegen.ML Tools/datatype_package.ML				\
+  Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
+  Tools/datatype_rep_proofs.ML Tools/inductive_codegen.ML			\
+  Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML		\
+  Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/prop_logic.ML		\
+  Tools/recdef_package.ML Tools/recfun_codegen.ML				\
+  Tools/reconstruction.ML Tools/record_package.ML Tools/refute.ML		\
+  Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML			\
+  Tools/res_clause.ML Tools/res_lib.ML Tools/res_skolem_function.ML		\
+  Tools/res_types_sorts.ML Tools/rewrite_hol_proof.ML				\
+  Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML	\
+  Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy		\
+  Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy		\
+  antisym_setup.ML arith_data.ML blastdata.ML cladata.ML			\
+  document/root.tex eqrule_HOL_data.ML hologic.ML simpdata.ML			\
+  thy_syntax.ML
 	@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
 
 
@@ -126,14 +121,15 @@
 
 HOL-Complex-HahnBanach: HOL-Complex $(LOG)/HOL-Complex-HahnBanach.gz
 
-$(LOG)/HOL-Complex-HahnBanach.gz: $(OUT)/HOL-Complex Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
-  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
-  Real/HahnBanach/HahnBanachExtLemmas.thy	\
-  Real/HahnBanach/HahnBanachSupLemmas.thy	\
-  Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
-  Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
-  Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
-  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \
+$(LOG)/HOL-Complex-HahnBanach.gz: $(OUT)/HOL-Complex			\
+  Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy		\
+  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy	\
+  Real/HahnBanach/HahnBanachExtLemmas.thy				\
+  Real/HahnBanach/HahnBanachSupLemmas.thy				\
+  Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy	\
+  Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML			\
+  Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy		\
+  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib	\
   Real/HahnBanach/document/root.tex
 	@cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL-Complex HahnBanach
 
@@ -142,24 +138,23 @@
 
 HOL-Complex: HOL $(OUT)/HOL-Complex
 
-$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML\
-  Library/Zorn.thy\
-  Real/Lubs.thy Real/rat_arith.ML\
-  Real/Rational.thy Real/PReal.thy Real/RComplete.thy \
-  Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy \
-  Real/RealPow.thy Real/document/root.tex\
-  Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy\
-  Hyperreal/Filter.thy Hyperreal/HSeries.thy\
-  Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\
-  Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
-  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
-  Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy\
-  Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\
-  Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy\
-  Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy \
-  Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
-  Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy\
-  Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy\
+$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML Library/Zorn.thy			\
+  Real/Lubs.thy Real/rat_arith.ML						\
+  Real/Rational.thy Real/PReal.thy Real/RComplete.thy				\
+  Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy		\
+  Real/RealPow.thy Real/document/root.tex					\
+  Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy			\
+  Hyperreal/Filter.thy Hyperreal/HSeries.thy					\
+  Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy			\
+  Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy					\
+  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy				\
+  Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy			\
+  Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy					\
+  Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy			\
+  Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy			\
+  Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML	\
+  Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy			\
+  Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy			\
   Complex/NSCA.thy Complex/NSComplex.thy Complex/document/root.tex 
 	@cd Complex; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Complex
 
--- a/src/HOL/ROOT.ML	Sun May 22 16:51:06 2005 +0200
+++ b/src/HOL/ROOT.ML	Sun May 22 16:51:07 2005 +0200
@@ -16,7 +16,6 @@
 
 use "hologic.ML";
 
-use "~~/src/Provers/simplifier.ML";
 use "~~/src/Provers/splitter.ML";
 use "~~/src/Provers/hypsubst.ML";
 use "~~/src/Provers/induct_method.ML";
--- a/src/Provers/README	Sun May 22 16:51:06 2005 +0200
+++ b/src/Provers/README	Sun May 22 16:51:07 2005 +0200
@@ -14,9 +14,8 @@
   linorder.ML		transitivity reasoner for linear (total) orders
   quantifier1.ML	simplification procedures for "1 point rules"
   simp.ML               powerful but slow simplifier
-  simplifier.ML         fast simplifier
   split_paired_all.ML	turn surjective pairing into split rule
-  splitter.ML           performs case splits for simplifier.ML
+  splitter.ML           performs case splits for simplifier
   typedsimp.ML          basic simplifier for explicitly typed logics
 
 directory Arith:
--- a/src/Provers/clasimp.ML	Sun May 22 16:51:06 2005 +0200
+++ b/src/Provers/clasimp.ML	Sun May 22 16:51:07 2005 +0200
@@ -3,7 +3,7 @@
     Author:     David von Oheimb, TU Muenchen
 
 Combination of classical reasoner and simplifier (depends on
-simplifier.ML, splitter.ML classical.ML, blast.ML).
+splitter.ML, classical.ML, blast.ML).
 *)
 
 infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2
--- a/src/Sequents/LK0.thy	Sun May 22 16:51:06 2005 +0200
+++ b/src/Sequents/LK0.thy	Sun May 22 16:51:07 2005 +0200
@@ -123,10 +123,6 @@
   If :: [o, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
    "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
 
-
-setup
-  Simplifier.setup
-
 setup
   prover_setup
 
--- a/src/Sequents/ROOT.ML	Sun May 22 16:51:06 2005 +0200
+++ b/src/Sequents/ROOT.ML	Sun May 22 16:51:07 2005 +0200
@@ -14,8 +14,6 @@
 Unify.trace_bound:= 20;
 Unify.search_bound := 40;
 
-use "~~/src/Provers/simplifier.ML";
-
 use_thy "Sequents";
 use "prover.ML";
isabelle