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.
Deleted semicolon at the end of the qed_goal line, which was preventing
authorlcp
Fri, 20 Jan 1995 02:00:23 +0100
changeset 868 452f1e6ae3bc
parent 867 e1a654c29b05
child 869 242b5050c1a6
Deleted semicolon at the end of the qed_goal line, which was preventing not_emptyE from being proved.
src/ZF/ZF.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/ZF.ML	Thu Jan 19 19:46:49 1995 +0100
+++ b/src/ZF/ZF.ML	Fri Jan 20 02:00:23 1995 +0100
@@ -405,7 +405,7 @@
 qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0"
  (fn _ => [REPEAT (ares_tac [notI, equals0D] 1)]);
 
-qed_goal "not_emptyE" ZF.thy "[| A ~= 0;  !!x. x:A ==> R |] ==> R";
+qed_goal "not_emptyE" ZF.thy "[| A ~= 0;  !!x. x:A ==> R |] ==> R"
  (fn [major,minor]=>
   [ rtac ([major, equals0I] MRS swap) 1,
     swap_res_tac [minor] 1,
isabelle