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.
fixed rulify_prems;
authorwenzelm
Fri, 01 Sep 2000 00:28:27 +0200
changeset 9769 a73540153a73
parent 9768 a589b1d75b7b
child 9770 5258ef87e85a
fixed rulify_prems;
src/HOL/Set.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Set.ML	Fri Sep 01 00:28:06 2000 +0200
+++ b/src/HOL/Set.ML	Fri Sep 01 00:28:27 2000 +0200
@@ -785,7 +785,7 @@
 
 fun gen_rulify_prems x =
   Attrib.no_args (Drule.rule_attribute (fn _ => (standard o
-    rule_by_tactic (REPEAT (ALLGOALS (resolve_tac [allI, ballI, impI])))))) x;
+    rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, ballI, impI])))))) x;
 
 in
isabelle