src/HOL/ROOT.ML
changeset 1024 b86042000035
parent 923 ff1574a81019
child 1165 97b2bb5d43c3
     1.1 --- a/src/HOL/ROOT.ML	Mon Apr 10 08:13:13 1995 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Mon Apr 10 08:40:58 1995 +0200
     1.3 @@ -18,17 +18,19 @@
     1.4  use "thy_syntax.ML";
     1.5  
     1.6  use_thy "HOL";
     1.7 +use "../Provers/simplifier.ML";
     1.8 +use "../Provers/splitter.ML";
     1.9  use "../Provers/hypsubst.ML";
    1.10  use "../Provers/classical.ML";
    1.11 -use "../Provers/simplifier.ML";
    1.12 -use "../Provers/splitter.ML";
    1.13  
    1.14  (** Applying HypsubstFun to generate hyp_subst_tac **)
    1.15  
    1.16  structure Hypsubst_Data =
    1.17    struct
    1.18 +  structure Simplifier = Simplifier
    1.19    (*Take apart an equality judgement; otherwise raise Match!*)
    1.20    fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
    1.21 +  val eq_reflection = eq_reflection
    1.22    val imp_intr = impI
    1.23    val rev_mp = rev_mp
    1.24    val subst = subst