--- a/ROOT.ML Thu Apr 06 11:21:13 1995 +0200
+++ b/ROOT.ML Thu Apr 06 11:24:11 1995 +0200
@@ -18,17 +18,19 @@
use "thy_syntax.ML";
use_thy "HOL";
+use "../Provers/simplifier.ML";
+use "../Provers/splitter.ML";
use "../Provers/hypsubst.ML";
use "../Provers/classical.ML";
-use "../Provers/simplifier.ML";
-use "../Provers/splitter.ML";
(** Applying HypsubstFun to generate hyp_subst_tac **)
structure Hypsubst_Data =
struct
+ structure Simplifier = Simplifier
(*Take apart an equality judgement; otherwise raise Match!*)
fun dest_eq (Const("Trueprop",_) $ (Const("op =",_) $ t $ u)) = (t,u);
+ val eq_reflection = eq_reflection
val imp_intr = impI
val rev_mp = rev_mp
val subst = subst