Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
arith method: HEADGOAL;
authorwenzelm
Fri, 24 Mar 2000 20:59:15 +0100
changeset 8571c323613e4a47
parent 8570 63d4f3ea2e70
child 8572 794843a9d8b1
arith method: HEADGOAL;
src/HOL/Arith.ML file | annotate | diff | comparison | revisions 
     1.1 --- a/src/HOL/Arith.ML	Fri Mar 24 17:29:51 2000 +0100
     1.2 +++ b/src/HOL/Arith.ML	Fri Mar 24 20:59:15 2000 +0100
     1.3 @@ -1034,7 +1034,7 @@
     1.4  (* proof method setup *)
     1.5  
     1.6  fun arith_method prems =
     1.7 -  Method.METHOD (fn facts => FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
     1.8 +  Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
     1.9  
    1.10  val arith_setup =
    1.11   [Method.add_methods
wneuper/isa