Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/eqrule_HOL_data.ML
changeset 18591 04b9f2bf5a48
parent 17521 0f1c48de39f5 
--- a/src/HOL/eqrule_HOL_data.ML	Fri Jan 06 15:18:19 2006 +0100
+++ b/src/HOL/eqrule_HOL_data.ML	Fri Jan 06 15:18:20 2006 +0100
@@ -1,6 +1,5 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      HOL/eqrule_HOL_data.ML
-    Id:		$Id$
+(*  ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
                 lucas.dixon@ed.ac.uk
     Modified:   22 July 2004
@@ -61,9 +60,4 @@
 
 end;
 
-structure EqRuleData = HOL_EqRuleData;
-
-structure EQSubstTac = 
-  EQSubstTacFUN(structure EqRuleData = EqRuleData);
-
-
+structure EqSubst = EqSubstFun(HOL_EqRuleData);
isabelle