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.
arith method: HEADGOAL;
authorwenzelm
Fri, 24 Mar 2000 20:59:15 +0100
changeset 8571 c323613e4a47
parent 8570 63d4f3ea2e70
child 8572 794843a9d8b1
arith method: HEADGOAL;
src/HOL/Arith.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Arith.ML	Fri Mar 24 17:29:51 2000 +0100
+++ b/src/HOL/Arith.ML	Fri Mar 24 20:59:15 2000 +0100
@@ -1034,7 +1034,7 @@
 (* proof method setup *)
 
 fun arith_method prems =
-  Method.METHOD (fn facts => FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
+  Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
 
 val arith_setup =
  [Method.add_methods
isabelle