Mercurial Mercurial > repos > Old_HOL / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Set up for new hyp_subst_tac.
authorlcp
Thu, 06 Apr 1995 11:24:11 +0200
changeset 240 2209eb5bb56b
parent 239 e65129244146
child 241 b67c8e01ae04
Set up for new hyp_subst_tac.
ROOT.ML file | annotate | diff | comparison | revisions 
--- 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
Old_HOL