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.
Tactic.precise_conjunction_tac;
authorwenzelm
Thu, 22 Dec 2005 00:28:53 +0100
changeset 18467 bb7b309ac395
parent 18466 389a6f9c31f4
child 18468 43951ffb6304
Tactic.precise_conjunction_tac;
src/Pure/axclass.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/axclass.ML	Thu Dec 22 00:28:52 2005 +0100
+++ b/src/Pure/axclass.ML	Thu Dec 22 00:28:53 2005 +0100
@@ -283,8 +283,9 @@
     val _ = message ("Proving type arity " ^ txt ^ " ...");
     val props = (mk_arities arity);
     val ths = Goal.prove_multi thy [] [] props
-      (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac) handle ERROR_MESSAGE msg =>
-        error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
+      (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac)
+        handle ERROR_MESSAGE msg =>
+          error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
   in add_arity_thms ths thy end;
 
 in
isabelle