src/HOL/Set.ML
changeset 10832 e33b47e4246d
parent 10482 41de88cb2108
child 11007 438f31613093
     1.1 --- a/src/HOL/Set.ML	Tue Jan 09 15:18:07 2001 +0100
     1.2 +++ b/src/HOL/Set.ML	Tue Jan 09 15:22:13 2001 +0100
     1.3 @@ -531,7 +531,7 @@
     1.4  Addsimps [singleton_conv2];
     1.5  
     1.6  
     1.7 -section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
     1.8 +section "Unions of families -- UNION x:A. B(x) is Union(B`A)";
     1.9  
    1.10  Goalw [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))";
    1.11  by (Blast_tac 1);
    1.12 @@ -561,7 +561,7 @@
    1.13  Addcongs [UN_cong];
    1.14  
    1.15  
    1.16 -section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
    1.17 +section "Intersections of families -- INTER x:A. B(x) is Inter(B`A)";
    1.18  
    1.19  Goalw [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))";
    1.20  by Auto_tac;
    1.21 @@ -652,7 +652,7 @@
    1.22  (*** Image of a set under a function ***)
    1.23  
    1.24  (*Frequently b does not have the syntactic form of f(x).*)
    1.25 -Goalw [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
    1.26 +Goalw [image_def] "[| b=f(x);  x:A |] ==> b : f`A";
    1.27  by (Blast_tac 1);
    1.28  qed "image_eqI";
    1.29  Addsimps [image_eqI];
    1.30 @@ -660,13 +660,13 @@
    1.31  bind_thm ("imageI", refl RS image_eqI);
    1.32  
    1.33  (*This version's more effective when we already have the required x*)
    1.34 -Goalw [image_def] "[| x:A;  b=f(x) |] ==> b : f``A";
    1.35 +Goalw [image_def] "[| x:A;  b=f(x) |] ==> b : f`A";
    1.36  by (Blast_tac 1);
    1.37  qed "rev_image_eqI";
    1.38  
    1.39  (*The eta-expansion gives variable-name preservation.*)
    1.40  val major::prems = Goalw [image_def]
    1.41 -    "[| b : (%x. f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
    1.42 +    "[| b : (%x. f(x))`A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
    1.43  by (rtac (major RS CollectD RS bexE) 1);
    1.44  by (REPEAT (ares_tac prems 1));
    1.45  qed "imageE";
    1.46 @@ -674,22 +674,22 @@
    1.47  AddIs  [image_eqI];
    1.48  AddSEs [imageE]; 
    1.49  
    1.50 -Goal "f``(A Un B) = f``A Un f``B";
    1.51 +Goal "f`(A Un B) = f`A Un f`B";
    1.52  by (Blast_tac 1);
    1.53  qed "image_Un";
    1.54  
    1.55 -Goal "(z : f``A) = (EX x:A. z = f x)";
    1.56 +Goal "(z : f`A) = (EX x:A. z = f x)";
    1.57  by (Blast_tac 1);
    1.58  qed "image_iff";
    1.59  
    1.60  (*This rewrite rule would confuse users if made default.*)
    1.61 -Goal "(f``A <= B) = (ALL x:A. f(x): B)";
    1.62 +Goal "(f`A <= B) = (ALL x:A. f(x): B)";
    1.63  by (Blast_tac 1);
    1.64  qed "image_subset_iff";
    1.65  
    1.66  (*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
    1.67    many existing proofs.*)
    1.68 -val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
    1.69 +val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f`A <= B";
    1.70  by (blast_tac (claset() addIs prems) 1);
    1.71  qed "image_subsetI";
    1.72