--- a/src/ZF/Rel.ML Mon Jun 22 15:53:24 1998 +0200
+++ b/src/ZF/Rel.ML Mon Jun 22 17:12:27 1998 +0200
@@ -29,7 +29,7 @@
by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
qed "symI";
-goalw Rel.thy [sym_def] "!!r. [| sym(r); <x,y>: r |] ==> <y,x>: r";
+Goalw [sym_def] "!!r. [| sym(r); <x,y>: r |] ==> <y,x>: r";
by (Blast_tac 1);
qed "symE";
@@ -48,12 +48,12 @@
(* transitivity *)
-goalw Rel.thy [trans_def]
+Goalw [trans_def]
"!!r. [| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
by (Blast_tac 1);
qed "transD";
-goalw Rel.thy [trans_on_def]
+Goalw [trans_on_def]
"!!r. [| trans[A](r); <a,b>:r; <b,c>:r; a:A; b:A; c:A |] ==> <a,c>:r";
by (Blast_tac 1);
qed "trans_onD";