--- a/src/ZF/AC/WO1_WO8.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/WO1_WO8.ML Tue Jul 25 17:31:53 1995 +0200
@@ -11,7 +11,7 @@
goalw thy WO_defs "!!Z. WO1 ==> WO8";
by (fast_tac ZF_cs 1);
-result();
+qed "WO1_WO8";
(* ********************************************************************** *)
(* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *)
@@ -27,4 +27,4 @@
by (fast_tac (ZF_cs addSEs [RepFunE, singleton_eq_iff RS iffD1 RS sym]
addSIs [lam_type, singletonI]
addIs [the_equality RS ssubst]) 1);
-result();
\ No newline at end of file
+qed "WO8_WO1";