src/ZF/Rel.ML

 (*  Title:      ZF/Rel.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-For Rel.thy.  Relations in Zermelo-Fraenkel Set Theory 
+Relations in Zermelo-Fraenkel Set Theory 
 *)
 
 open Rel;
 
 (*** Some properties of relations -- useful? ***)

 qed "antisymE";
 
 (* transitivity *)
 
 Goalw [trans_def]
-    "!!r. [| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r";
+    "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r";
 by (Blast_tac 1);
 qed "transD";
 
 Goalw [trans_on_def]
-    "!!r. [| trans[A](r);  <a,b>:r;  <b,c>:r;  a:A;  b:A;  c:A |] ==> <a,c>: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";