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.
improved asm_finish;
authorwenzelm
Tue, 12 Jan 1999 16:44:31 +0100
changeset 6104 55c7f8f0bb4d
parent 6103 36f272ea9413
child 6105 b4ec1af7053f
improved asm_finish;
src/Pure/Isar/method.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/method.ML	Tue Jan 12 16:42:21 1999 +0100
+++ b/src/Pure/Isar/method.ML	Tue Jan 12 16:44:31 1999 +0100
@@ -92,7 +92,7 @@
 val trivial = METHOD (ALLGOALS o trivial_tac);
 val assumption = METHOD (fn facts => FIRSTGOAL (trivial_tac facts THEN' assume_tac));
 
-val asm_finish = METHOD (K (TRYALL assume_tac));
+val asm_finish = METHOD (K (FILTER (equal 0 o Thm.nprems_of) (ALLGOALS assume_tac)));
 
 
 (* rule *)
isabelle