1.1 --- a/src/HOL/HOL.ML	Fri Nov 17 12:08:04 1995 +0100
     1.2 +++ b/src/HOL/HOL.ML	Fri Nov 17 12:19:21 1995 +0100
     1.3 @@ -268,3 +268,47 @@
     1.4  fun stac th = rtac(th RS ssubst);
     1.5  fun sstac ths = EVERY' (map stac ths);
     1.6  fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
     1.7 +
     1.8 +
     1.9 +(*** Load simpdata.ML to be able to initialize HOL's simpset ***)
    1.10 +
    1.11 +(** Applying HypsubstFun to generate hyp_subst_tac **)
    1.12 +
    1.13 +structure Hypsubst_Data =
    1.14 +  struct
    1.15 +  structure Simplifier = Simplifier
    1.16 +  (*Take apart an equality judgement; otherwise raise Match!*)
    1.17 +  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
    1.18 +  val eq_reflection = eq_reflection
    1.19 +  val imp_intr = impI
    1.20 +  val rev_mp = rev_mp
    1.21 +  val subst = subst
    1.22 +  val sym = sym
    1.23 +  end;
    1.24 +
    1.25 +structure Hypsubst = HypsubstFun(Hypsubst_Data);
    1.26 +open Hypsubst;
    1.27 +
    1.28 +(*** Applying ClassicalFun to create a classical prover ***)
    1.29 +structure Classical_Data = 
    1.30 +  struct
    1.31 +  val sizef	= size_of_thm
    1.32 +  val mp	= mp
    1.33 +  val not_elim	= notE
    1.34 +  val classical	= classical
    1.35 +  val hyp_subst_tacs=[hyp_subst_tac]
    1.36 +  end;
    1.37 +
    1.38 +structure Classical = ClassicalFun(Classical_Data);
    1.39 +open Classical;
    1.40 +
    1.41 +(*Propositional rules*)
    1.42 +val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
    1.43 +                       addSEs [conjE,disjE,impCE,FalseE,iffE];
    1.44 +
    1.45 +(*Quantifier rules*)
    1.46 +val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
    1.47 +                     addSEs [exE,ex1E] addEs [allE];
    1.48 +
    1.49 +use     "simpdata.ML";
    1.50 +simpset := HOL_ss;

     2.1 --- a/src/HOL/ROOT.ML	Fri Nov 17 12:08:04 1995 +0100
     2.2 +++ b/src/HOL/ROOT.ML	Fri Nov 17 12:19:21 1995 +0100
     2.3 @@ -16,50 +16,12 @@
     2.4  use "../Pure/section_utils.ML";
     2.5  use "thy_syntax.ML";
     2.6  
     2.7 -use_thy "HOL";
     2.8  use "../Provers/splitter.ML";
     2.9  use "../Provers/hypsubst.ML";
    2.10  use "../Provers/classical.ML";
    2.11  
    2.12 -(** Applying HypsubstFun to generate hyp_subst_tac **)
    2.13  
    2.14 -structure Hypsubst_Data =
    2.15 -  struct
    2.16 -  structure Simplifier = Simplifier
    2.17 -  (*Take apart an equality judgement; otherwise raise Match!*)
    2.18 -  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
    2.19 -  val eq_reflection = eq_reflection
    2.20 -  val imp_intr = impI
    2.21 -  val rev_mp = rev_mp
    2.22 -  val subst = subst
    2.23 -  val sym = sym
    2.24 -  end;
    2.25 -
    2.26 -structure Hypsubst = HypsubstFun(Hypsubst_Data);
    2.27 -open Hypsubst;
    2.28 -
    2.29 -(*** Applying ClassicalFun to create a classical prover ***)
    2.30 -structure Classical_Data = 
    2.31 -  struct
    2.32 -  val sizef	= size_of_thm
    2.33 -  val mp	= mp
    2.34 -  val not_elim	= notE
    2.35 -  val classical	= classical
    2.36 -  val hyp_subst_tacs=[hyp_subst_tac]
    2.37 -  end;
    2.38 -
    2.39 -structure Classical = ClassicalFun(Classical_Data);
    2.40 -open Classical;
    2.41 -
    2.42 -(*Propositional rules*)
    2.43 -val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
    2.44 -                       addSEs [conjE,disjE,impCE,FalseE,iffE];
    2.45 -
    2.46 -(*Quantifier rules*)
    2.47 -val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
    2.48 -                     addSEs [exE,ex1E] addEs [allE];
    2.49 -
    2.50 -use     "simpdata.ML";
    2.51 +use_thy "HOL";
    2.52  
    2.53  use_thy "Ord";
    2.54  use_thy "subset";