src/HOL/ROOT.ML
changeset 1338 d2fc3bfaee7f
parent 1301 42782316d510
child 1358 0b63af4a2627
     1.1 --- a/src/HOL/ROOT.ML	Fri Nov 17 12:08:04 1995 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Fri Nov 17 12:19:21 1995 +0100
     1.3 @@ -16,50 +16,12 @@
     1.4  use "../Pure/section_utils.ML";
     1.5  use "thy_syntax.ML";
     1.6  
     1.7 -use_thy "HOL";
     1.8  use "../Provers/splitter.ML";
     1.9  use "../Provers/hypsubst.ML";
    1.10  use "../Provers/classical.ML";
    1.11  
    1.12 -(** Applying HypsubstFun to generate hyp_subst_tac **)
    1.13  
    1.14 -structure Hypsubst_Data =
    1.15 -  struct
    1.16 -  structure Simplifier = Simplifier
    1.17 -  (*Take apart an equality judgement; otherwise raise Match!*)
    1.18 -  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
    1.19 -  val eq_reflection = eq_reflection
    1.20 -  val imp_intr = impI
    1.21 -  val rev_mp = rev_mp
    1.22 -  val subst = subst
    1.23 -  val sym = sym
    1.24 -  end;
    1.25 -
    1.26 -structure Hypsubst = HypsubstFun(Hypsubst_Data);
    1.27 -open Hypsubst;
    1.28 -
    1.29 -(*** Applying ClassicalFun to create a classical prover ***)
    1.30 -structure Classical_Data = 
    1.31 -  struct
    1.32 -  val sizef	= size_of_thm
    1.33 -  val mp	= mp
    1.34 -  val not_elim	= notE
    1.35 -  val classical	= classical
    1.36 -  val hyp_subst_tacs=[hyp_subst_tac]
    1.37 -  end;
    1.38 -
    1.39 -structure Classical = ClassicalFun(Classical_Data);
    1.40 -open Classical;
    1.41 -
    1.42 -(*Propositional rules*)
    1.43 -val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
    1.44 -                       addSEs [conjE,disjE,impCE,FalseE,iffE];
    1.45 -
    1.46 -(*Quantifier rules*)
    1.47 -val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
    1.48 -                     addSEs [exE,ex1E] addEs [allE];
    1.49 -
    1.50 -use     "simpdata.ML";
    1.51 +use_thy "HOL";
    1.52  
    1.53  use_thy "Ord";
    1.54  use_thy "subset";