# HG changeset patch
# User lcp
# Date 790563623 -3600
# Node ID 452f1e6ae3bc5e5289debc3cf5bda9dfe313c4b9
# Parent  e1a654c29b05c87465679a92d61fe00ce46697bd
Deleted semicolon at the end of the qed_goal line, which was preventing
not_emptyE from being proved.

diff -r e1a654c29b05 -r 452f1e6ae3bc src/ZF/ZF.ML
--- 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,