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: bang arg;
authorwenzelm
Fri, 17 Mar 2000 17:11:59 +0100
changeset 8502 75fc67e56440
parent 8501 2ff3d25943f1
child 8503 9d62b37bbfca
arith method: bang arg;
src/HOL/Arith.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Arith.ML	Fri Mar 17 17:10:37 2000 +0100
+++ b/src/HOL/Arith.ML	Fri Mar 17 17:11:59 2000 +0100
@@ -1033,12 +1033,12 @@
 
 (* proof method setup *)
 
-val arith_method =
-  Method.METHOD (fn facts => FIRSTGOAL (Method.insert_tac facts THEN' arith_tac));
+fun arith_method prems =
+  Method.METHOD (fn facts => FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
 
 val arith_setup =
  [Method.add_methods
-  [("arith", Method.no_args arith_method, "decide linear arithmethic")]];
+  [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts , "decide linear arithmethic")]];
 
 (*---------------------------------------------------------------------------*)
 (* End of proof procedures. Now go and USE them!                             *)
isabelle