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";