src/HOL/Set.ML
changeset 5143 b94cd208f073
parent 5069 3ea049f7979d
child 5148 74919e8f221c
     1.1 --- a/src/HOL/Set.ML	Tue Jul 14 13:33:12 1998 +0200
     1.2 +++ b/src/HOL/Set.ML	Wed Jul 15 10:15:13 1998 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  Addsimps [Collect_mem_eq];
     1.5  AddIffs  [mem_Collect_eq];
     1.6  
     1.7 -Goal "!!a. P(a) ==> a : {x. P(x)}";
     1.8 +Goal "P(a) ==> a : {x. P(x)}";
     1.9  by (Asm_simp_tac 1);
    1.10  qed "CollectI";
    1.11  
    1.12 @@ -325,11 +325,11 @@
    1.13  
    1.14  Addsimps [Un_iff];
    1.15  
    1.16 -Goal "!!c. c:A ==> c : A Un B";
    1.17 +Goal "c:A ==> c : A Un B";
    1.18  by (Asm_simp_tac 1);
    1.19  qed "UnI1";
    1.20  
    1.21 -Goal "!!c. c:B ==> c : A Un B";
    1.22 +Goal "c:B ==> c : A Un B";
    1.23  by (Asm_simp_tac 1);
    1.24  qed "UnI2";
    1.25  
    1.26 @@ -356,15 +356,15 @@
    1.27  
    1.28  Addsimps [Int_iff];
    1.29  
    1.30 -Goal "!!c. [| c:A;  c:B |] ==> c : A Int B";
    1.31 +Goal "[| c:A;  c:B |] ==> c : A Int B";
    1.32  by (Asm_simp_tac 1);
    1.33  qed "IntI";
    1.34  
    1.35 -Goal "!!c. c : A Int B ==> c:A";
    1.36 +Goal "c : A Int B ==> c:A";
    1.37  by (Asm_full_simp_tac 1);
    1.38  qed "IntD1";
    1.39  
    1.40 -Goal "!!c. c : A Int B ==> c:B";
    1.41 +Goal "c : A Int B ==> c:B";
    1.42  by (Asm_full_simp_tac 1);
    1.43  qed "IntD2";
    1.44  
    1.45 @@ -436,7 +436,7 @@
    1.46  qed_goal "singletonI" Set.thy "a : {a}"
    1.47   (fn _=> [ (rtac insertI1 1) ]);
    1.48  
    1.49 -Goal "!!a. b : {a} ==> b=a";
    1.50 +Goal "b : {a} ==> b=a";
    1.51  by (Blast_tac 1);
    1.52  qed "singletonD";
    1.53  
    1.54 @@ -445,7 +445,7 @@
    1.55  qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" 
    1.56  (fn _ => [Blast_tac 1]);
    1.57  
    1.58 -Goal "!!a b. {a}={b} ==> a=b";
    1.59 +Goal "{a}={b} ==> a=b";
    1.60  by (blast_tac (claset() addEs [equalityE]) 1);
    1.61  qed "singleton_inject";
    1.62  
    1.63 @@ -469,7 +469,7 @@
    1.64  Addsimps [UN_iff];
    1.65  
    1.66  (*The order of the premises presupposes that A is rigid; b may be flexible*)
    1.67 -Goal "!!b. [| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
    1.68 +Goal "[| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
    1.69  by Auto_tac;
    1.70  qed "UN_I";
    1.71  
    1.72 @@ -504,7 +504,7 @@
    1.73  by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
    1.74  qed "INT_I";
    1.75  
    1.76 -Goal "!!b. [| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
    1.77 +Goal "[| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
    1.78  by Auto_tac;
    1.79  qed "INT_D";
    1.80  
    1.81 @@ -536,7 +536,7 @@
    1.82  Addsimps [Union_iff];
    1.83  
    1.84  (*The order of the premises presupposes that C is rigid; A may be flexible*)
    1.85 -Goal "!!X. [| X:C;  A:X |] ==> A : Union(C)";
    1.86 +Goal "[| X:C;  A:X |] ==> A : Union(C)";
    1.87  by Auto_tac;
    1.88  qed "UnionI";
    1.89  
    1.90 @@ -565,7 +565,7 @@
    1.91  
    1.92  (*A "destruct" rule -- every X in C contains A as an element, but
    1.93    A:X can hold when X:C does not!  This rule is analogous to "spec". *)
    1.94 -Goal "!!X. [| A : Inter(C);  X:C |] ==> A:X";
    1.95 +Goal "[| A : Inter(C);  X:C |] ==> A:X";
    1.96  by Auto_tac;
    1.97  qed "InterD";
    1.98  
    1.99 @@ -626,7 +626,7 @@
   1.100  
   1.101  (*** Range of a function -- just a translation for image! ***)
   1.102  
   1.103 -Goal "!!b. b=f(x) ==> b : range(f)";
   1.104 +Goal "b=f(x) ==> b : range(f)";
   1.105  by (EVERY1 [etac image_eqI, rtac UNIV_I]);
   1.106  bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI));
   1.107