src/HOL/Relation.ML
changeset 5143 b94cd208f073
parent 5069 3ea049f7979d
child 5148 74919e8f221c
     1.1 --- a/src/HOL/Relation.ML	Tue Jul 14 13:33:12 1998 +0200
     1.2 +++ b/src/HOL/Relation.ML	Wed Jul 15 10:15:13 1998 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  by (Blast_tac 1);
     1.5  qed "O_assoc";
     1.6  
     1.7 -Goal "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
     1.8 +Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
     1.9  by (Blast_tac 1);
    1.10  qed "comp_mono";
    1.11  
    1.12 @@ -91,17 +91,17 @@
    1.13  
    1.14  (** Natural deduction for r^-1 **)
    1.15  
    1.16 -Goalw [converse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
    1.17 +Goalw [converse_def] "((a,b): r^-1) = ((b,a):r)";
    1.18  by (Simp_tac 1);
    1.19  qed "converse_iff";
    1.20  
    1.21  AddIffs [converse_iff];
    1.22  
    1.23 -Goalw [converse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
    1.24 +Goalw [converse_def] "(a,b):r ==> (b,a): r^-1";
    1.25  by (Simp_tac 1);
    1.26  qed "converseI";
    1.27  
    1.28 -Goalw [converse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
    1.29 +Goalw [converse_def] "(a,b) : r^-1 ==> (b,a) : r";
    1.30  by (Blast_tac 1);
    1.31  qed "converseD";
    1.32