Mercurial Mercurial > repos > isabelle / 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.
Removed structure Prod_Syntax.
authorberghofe
Tue, 30 Jun 1998 20:57:46 +0200
changeset 5103 866a281a8c2a
parent 5102 8c782c25a11e
child 5104 230cca8452c7
Removed structure Prod_Syntax.
TFL/post.sml file | annotate | diff | comparison | revisions 
--- a/TFL/post.sml	Tue Jun 30 20:51:15 1998 +0200
+++ b/TFL/post.sml	Tue Jun 30 20:57:46 1998 +0200
@@ -168,7 +168,7 @@
 
 
 (*lcp: curry the predicate of the induction rule*)
-fun curry_rule rl = Prod_Syntax.split_rule_var
+fun curry_rule rl = split_rule_var
                         (head_of (HOLogic.dest_Trueprop (concl_of rl)), 
 			 rl);
isabelle