`` -> and ``` -> ``
authornipkow
Tue Jan 09 15:22:13 2001 +0100 (2001-01-09)
changeset 10832e33b47e4246d
parent 10831 024bdf8e52a4
child 10833 c0844a30ea4e
`` -> and ``` -> ``
src/HOL/Datatype_Universe.thy
src/HOL/Finite.ML
src/HOL/Fun.ML
src/HOL/Inverse_Image.ML
src/HOL/Inverse_Image.thy
src/HOL/List.ML
src/HOL/List.thy
src/HOL/NatDef.ML
src/HOL/NatDef.thy
src/HOL/Product_Type.ML
src/HOL/Relation.ML
src/HOL/Relation.thy
src/HOL/Set.ML
src/HOL/Set.thy
src/HOL/Sum_Type.thy
src/HOL/Wellfounded_Recursion.ML
src/HOL/equalities.ML
src/HOL/mono.ML
     1.1 --- a/src/HOL/Datatype_Universe.thy	Tue Jan 09 15:18:07 2001 +0100
     1.2 +++ b/src/HOL/Datatype_Universe.thy	Tue Jan 09 15:22:13 2001 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4  
     1.5    (*S-expression constructors*)
     1.6    Atom_def   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
     1.7 -  Scons_def  "Scons M N == (Push_Node (Inr 1) `` M) Un (Push_Node (Inr 2) `` N)"
     1.8 +  Scons_def  "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr 2) ` N)"
     1.9  
    1.10    (*Leaf nodes, with arbitrary or nat labels*)
    1.11    Leaf_def   "Leaf == Atom o Inl"
    1.12 @@ -74,7 +74,7 @@
    1.13    In1_def    "In1(M) == Scons (Numb 1) M"
    1.14  
    1.15    (*Function spaces*)
    1.16 -  Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) `` (f x)}"
    1.17 +  Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}"
    1.18    Funs_def "Funs S == {f. range f <= S}"
    1.19  
    1.20    (*the set of nodes with depth less than k*)
    1.21 @@ -83,7 +83,7 @@
    1.22  
    1.23    (*products and sums for the "universe"*)
    1.24    uprod_def  "uprod A B == UN x:A. UN y:B. { Scons x y }"
    1.25 -  usum_def   "usum A B == In0``A Un In1``B"
    1.26 +  usum_def   "usum A B == In0`A Un In1`B"
    1.27  
    1.28    (*the corresponding eliminators*)
    1.29    Split_def  "Split c M == @u. ? x y. M = Scons x y & u = c x y"
     2.1 --- a/src/HOL/Finite.ML	Tue Jan 09 15:18:07 2001 +0100
     2.2 +++ b/src/HOL/Finite.ML	Tue Jan 09 15:22:13 2001 +0100
     2.3 @@ -74,7 +74,7 @@
     2.4  Addsimps[finite_insert];
     2.5  
     2.6  (*The image of a finite set is finite *)
     2.7 -Goal  "finite F ==> finite(h``F)";
     2.8 +Goal  "finite F ==> finite(h`F)";
     2.9  by (etac finite_induct 1);
    2.10  by (Simp_tac 1);
    2.11  by (Asm_simp_tac 1);
    2.12 @@ -127,11 +127,11 @@
    2.13  val lemma = result();
    2.14  
    2.15  (*Lemma for proving finite_imageD*)
    2.16 -Goal "finite B ==> ALL A. f``A = B --> inj_on f A --> finite A";
    2.17 +Goal "finite B ==> ALL A. f`A = B --> inj_on f A --> finite A";
    2.18  by (etac finite_induct 1);
    2.19   by (ALLGOALS Asm_simp_tac);
    2.20  by (Clarify_tac 1);
    2.21 -by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
    2.22 +by (subgoal_tac "EX y:A. f y = x & F = f`(A-{y})" 1);
    2.23   by (Clarify_tac 1);
    2.24   by (full_simp_tac (simpset() addsimps [inj_on_def]) 1);
    2.25   by (blast_tac (claset() addSDs [lemma RS iffD1]) 1);
    2.26 @@ -143,7 +143,7 @@
    2.27      (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff])));
    2.28  val lemma = result();
    2.29  
    2.30 -Goal "[| finite(f``A);  inj_on f A |] ==> finite A";
    2.31 +Goal "[| finite(f`A);  inj_on f A |] ==> finite A";
    2.32  by (dtac lemma 1);
    2.33  by (Blast_tac 1);
    2.34  qed "finite_imageD";
    2.35 @@ -195,7 +195,7 @@
    2.36  (** The powerset of a finite set **)
    2.37  
    2.38  Goal "finite(Pow A) ==> finite A";
    2.39 -by (subgoal_tac "finite ((%x.{x})``A)" 1);
    2.40 +by (subgoal_tac "finite ((%x.{x})`A)" 1);
    2.41  by (rtac finite_subset 2);
    2.42  by (assume_tac 3);
    2.43  by (ALLGOALS
    2.44 @@ -214,7 +214,7 @@
    2.45  AddIffs [finite_Pow_iff];
    2.46  
    2.47  Goal "finite(r^-1) = finite r";
    2.48 -by (subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
    2.49 +by (subgoal_tac "r^-1 = (%(x,y).(y,x))`r" 1);
    2.50   by (Asm_simp_tac 1);
    2.51   by (rtac iffI 1);
    2.52    by (etac (rewrite_rule [inj_on_def] finite_imageD) 1);
    2.53 @@ -467,14 +467,14 @@
    2.54  
    2.55  (*** Cardinality of image ***)
    2.56  
    2.57 -Goal "finite A ==> card (f `` A) <= card A";
    2.58 +Goal "finite A ==> card (f ` A) <= card A";
    2.59  by (etac finite_induct 1);
    2.60   by (Simp_tac 1);
    2.61  by (asm_simp_tac (simpset() addsimps [le_SucI, finite_imageI, 
    2.62  				      card_insert_if]) 1);
    2.63  qed "card_image_le";
    2.64  
    2.65 -Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A";
    2.66 +Goal "finite(A) ==> inj_on f A --> card (f ` A) = card A";
    2.67  by (etac finite_induct 1);
    2.68  by (ALLGOALS Asm_simp_tac);
    2.69  by Safe_tac;
    2.70 @@ -486,7 +486,7 @@
    2.71  by (Blast_tac 1);
    2.72  qed_spec_mp "card_image";
    2.73  
    2.74 -Goal "[| finite A; f``A <= A; inj_on f A |] ==> f``A = A";
    2.75 +Goal "[| finite A; f`A <= A; inj_on f A |] ==> f`A = A";
    2.76  by (asm_simp_tac (simpset() addsimps [card_seteq, card_image]) 1);
    2.77  qed "endo_inj_surj";
    2.78  
    2.79 @@ -853,14 +853,14 @@
    2.80  by (auto_tac (claset() addIs [finite_subset], simpset()));
    2.81  qed "choose_deconstruct";
    2.82  
    2.83 -Goal "[| finite(A); finite(B);  f``A <= B;  inj_on f A |] \
    2.84 +Goal "[| finite(A); finite(B);  f`A <= B;  inj_on f A |] \
    2.85  \     ==> card A <= card B";
    2.86  by (auto_tac (claset() addIs [card_mono], 
    2.87  	      simpset() addsimps [card_image RS sym]));
    2.88  qed "card_inj_on_le";
    2.89  
    2.90  Goal "[| finite A; finite B; \
    2.91 -\        f``A <= B; inj_on f A; g``B <= A; inj_on g B |] \
    2.92 +\        f`A <= B; inj_on f A; g`B <= A; inj_on g B |] \
    2.93  \     ==> card(A) = card(B)";
    2.94  by (auto_tac (claset() addIs [le_anti_sym,card_inj_on_le], simpset()));
    2.95  qed "card_bij_eq";
     3.1 --- a/src/HOL/Fun.ML	Tue Jan 09 15:18:07 2001 +0100
     3.2 +++ b/src/HOL/Fun.ML	Tue Jan 09 15:22:13 2001 +0100
     3.3 @@ -65,15 +65,15 @@
     3.4  qed "o_id";
     3.5  Addsimps [o_id];
     3.6  
     3.7 -Goalw [o_def] "(f o g)``r = f``(g``r)";
     3.8 +Goalw [o_def] "(f o g)`r = f`(g`r)";
     3.9  by (Blast_tac 1);
    3.10  qed "image_compose";
    3.11  
    3.12 -Goal "f``A = (UN x:A. {f x})";
    3.13 +Goal "f`A = (UN x:A. {f x})";
    3.14  by (Blast_tac 1);
    3.15  qed "image_eq_UN";
    3.16  
    3.17 -Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
    3.18 +Goalw [o_def] "UNION A (g o f) = UNION (f`A) g";
    3.19  by (Blast_tac 1);
    3.20  qed "UN_o";
    3.21  
    3.22 @@ -205,7 +205,7 @@
    3.23  
    3.24  (*** Lemmas about injective functions and inv ***)
    3.25  
    3.26 -Goalw [o_def] "[| inj_on f A;  inj_on g (f``A) |] ==> inj_on (g o f) A";
    3.27 +Goalw [o_def] "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A";
    3.28  by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
    3.29  qed "comp_inj_on";
    3.30  
    3.31 @@ -288,147 +288,147 @@
    3.32  (** We seem to need both the id-forms and the (%x. x) forms; the latter can
    3.33      arise by rewriting, while id may be used explicitly. **)
    3.34  
    3.35 -Goal "(%x. x) `` Y = Y";
    3.36 +Goal "(%x. x) ` Y = Y";
    3.37  by (Blast_tac 1);
    3.38  qed "image_ident";
    3.39  
    3.40 -Goalw [id_def] "id `` Y = Y";
    3.41 +Goalw [id_def] "id ` Y = Y";
    3.42  by (Blast_tac 1);
    3.43  qed "image_id";
    3.44  Addsimps [image_ident, image_id];
    3.45  
    3.46 -Goal "(%x. x) -`` Y = Y";
    3.47 +Goal "(%x. x) -` Y = Y";
    3.48  by (Blast_tac 1);
    3.49  qed "vimage_ident";
    3.50  
    3.51 -Goalw [id_def] "id -`` A = A";
    3.52 +Goalw [id_def] "id -` A = A";
    3.53  by Auto_tac;
    3.54  qed "vimage_id";
    3.55  Addsimps [vimage_ident, vimage_id];
    3.56  
    3.57 -Goal "f -`` (f `` A) = {y. EX x:A. f x = f y}";
    3.58 +Goal "f -` (f ` A) = {y. EX x:A. f x = f y}";
    3.59  by (blast_tac (claset() addIs [sym]) 1);
    3.60  qed "vimage_image_eq";
    3.61  
    3.62 -Goal "f `` (f -`` A) <= A";
    3.63 +Goal "f ` (f -` A) <= A";
    3.64  by (Blast_tac 1);
    3.65  qed "image_vimage_subset";
    3.66  
    3.67 -Goal "f `` (f -`` A) = A Int range f";
    3.68 +Goal "f ` (f -` A) = A Int range f";
    3.69  by (Blast_tac 1);
    3.70  qed "image_vimage_eq";
    3.71  Addsimps [image_vimage_eq];
    3.72  
    3.73 -Goal "surj f ==> f `` (f -`` A) = A";
    3.74 +Goal "surj f ==> f ` (f -` A) = A";
    3.75  by (asm_simp_tac (simpset() addsimps [surj_range]) 1);
    3.76  qed "surj_image_vimage_eq";
    3.77  
    3.78 -Goal "surj f ==> f `` (inv f `` A) = A";
    3.79 +Goal "surj f ==> f ` (inv f ` A) = A";
    3.80  by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1);
    3.81  qed "image_surj_f_inv_f";
    3.82  
    3.83 -Goalw [inj_on_def] "inj f ==> f -`` (f `` A) = A";
    3.84 +Goalw [inj_on_def] "inj f ==> f -` (f ` A) = A";
    3.85  by (Blast_tac 1);
    3.86  qed "inj_vimage_image_eq";
    3.87  
    3.88 -Goal "inj f ==> (inv f) `` (f `` A) = A";
    3.89 +Goal "inj f ==> (inv f) ` (f ` A) = A";
    3.90  by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1);
    3.91  qed "image_inv_f_f";
    3.92  
    3.93 -Goalw [surj_def] "surj f ==> f -`` B <= A ==> B <= f `` A";
    3.94 +Goalw [surj_def] "surj f ==> f -` B <= A ==> B <= f ` A";
    3.95  by (blast_tac (claset() addIs [sym]) 1);
    3.96  qed "vimage_subsetD";
    3.97  
    3.98 -Goalw [inj_on_def] "inj f ==> B <= f `` A ==> f -`` B <= A";
    3.99 +Goalw [inj_on_def] "inj f ==> B <= f ` A ==> f -` B <= A";
   3.100  by (Blast_tac 1);
   3.101  qed "vimage_subsetI";
   3.102  
   3.103 -Goalw [bij_def] "bij f ==> (f -`` B <= A) = (B <= f `` A)";
   3.104 +Goalw [bij_def] "bij f ==> (f -` B <= A) = (B <= f ` A)";
   3.105  by (blast_tac (claset() delrules [subsetI]
   3.106  			addIs [vimage_subsetI, vimage_subsetD]) 1);
   3.107  qed "vimage_subset_eq";
   3.108  
   3.109 -Goal "f``(A Int B) <= f``A Int f``B";
   3.110 +Goal "f`(A Int B) <= f`A Int f`B";
   3.111  by (Blast_tac 1);
   3.112  qed "image_Int_subset";
   3.113  
   3.114 -Goal "f``A - f``B <= f``(A - B)";
   3.115 +Goal "f`A - f`B <= f`(A - B)";
   3.116  by (Blast_tac 1);
   3.117  qed "image_diff_subset";
   3.118  
   3.119  Goalw [inj_on_def]
   3.120 -   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
   3.121 +   "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A Int B) = f`A Int f`B";
   3.122  by (Blast_tac 1);
   3.123  qed "inj_on_image_Int";
   3.124  
   3.125  Goalw [inj_on_def]
   3.126 -   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
   3.127 +   "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A-B) = f`A - f`B";
   3.128  by (Blast_tac 1);
   3.129  qed "inj_on_image_set_diff";
   3.130  
   3.131 -Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B";
   3.132 +Goalw [inj_on_def] "inj f ==> f`(A Int B) = f`A Int f`B";
   3.133  by (Blast_tac 1);
   3.134  qed "image_Int";
   3.135  
   3.136 -Goalw [inj_on_def] "inj f ==> f``(A-B) = f``A - f``B";
   3.137 +Goalw [inj_on_def] "inj f ==> f`(A-B) = f`A - f`B";
   3.138  by (Blast_tac 1);
   3.139  qed "image_set_diff";
   3.140  
   3.141 -Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X";
   3.142 +Goalw [image_def] "inj(f) ==> inv(f)`(f`X) = X";
   3.143  by Auto_tac;
   3.144  qed "inv_image_comp";
   3.145  
   3.146 -Goal "inj f ==> (f a : f``A) = (a : A)";
   3.147 +Goal "inj f ==> (f a : f`A) = (a : A)";
   3.148  by (blast_tac (claset() addDs [injD]) 1);
   3.149  qed "inj_image_mem_iff";
   3.150  
   3.151 -Goalw [inj_on_def] "inj f ==> (f``A <= f``B) = (A<=B)";
   3.152 +Goalw [inj_on_def] "inj f ==> (f`A <= f`B) = (A<=B)";
   3.153  by (Blast_tac 1);
   3.154  qed "inj_image_subset_iff";
   3.155  
   3.156 -Goal "inj f ==> (f``A = f``B) = (A = B)";
   3.157 +Goal "inj f ==> (f`A = f`B) = (A = B)";
   3.158  by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
   3.159  qed "inj_image_eq_iff";
   3.160  
   3.161 -Goal  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
   3.162 +Goal  "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))";
   3.163  by (Blast_tac 1);
   3.164  qed "image_UN";
   3.165  
   3.166  (*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
   3.167  Goalw [inj_on_def]
   3.168     "[| inj_on f C;  ALL x:A. B x <= C;  j:A |] \
   3.169 -\   ==> f `` (INTER A B) = (INT x:A. f `` B x)";
   3.170 +\   ==> f ` (INTER A B) = (INT x:A. f ` B x)";
   3.171  by (Blast_tac 1);
   3.172  qed "image_INT";
   3.173  
   3.174  (*Compare with image_INT: no use of inj_on, and if f is surjective then
   3.175    it doesn't matter whether A is empty*)
   3.176 -Goalw [bij_def] "bij f ==> f `` (INTER A B) = (INT x:A. f `` B x)";
   3.177 +Goalw [bij_def] "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)";
   3.178  by (force_tac (claset() addSIs [surj_f_inv_f RS sym RS image_eqI], 
   3.179  	       simpset()) 1);
   3.180  qed "bij_image_INT";
   3.181  
   3.182 -Goal "bij f ==> f `` Collect P = {y. P (inv f y)}";
   3.183 +Goal "bij f ==> f ` Collect P = {y. P (inv f y)}";
   3.184  by Auto_tac;
   3.185  by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1);
   3.186  by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1);
   3.187  qed "bij_image_Collect_eq";
   3.188  
   3.189 -Goal "bij f ==> f -`` A = inv f `` A";
   3.190 +Goal "bij f ==> f -` A = inv f ` A";
   3.191  by Safe_tac;
   3.192  by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
   3.193  by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
   3.194  qed "bij_vimage_eq_inv_image";
   3.195  
   3.196 -Goal "surj f ==> -(f``A) <= f``(-A)";
   3.197 +Goal "surj f ==> -(f`A) <= f`(-A)";
   3.198  by (auto_tac (claset(), simpset() addsimps [surj_def]));  
   3.199  qed "surj_Compl_image_subset";
   3.200  
   3.201 -Goal "inj f ==> f``(-A) <= -(f``A)";
   3.202 +Goal "inj f ==> f`(-A) <= -(f`A)";
   3.203  by (auto_tac (claset(), simpset() addsimps [inj_on_def]));  
   3.204  qed "inj_image_Compl_subset";
   3.205  
   3.206 -Goalw [bij_def] "bij f ==> f``(-A) = -(f``A)";
   3.207 +Goalw [bij_def] "bij f ==> f`(-A) = -(f`A)";
   3.208  by (rtac equalityI 1); 
   3.209  by (ALLGOALS (asm_simp_tac (simpset() addsimps [inj_image_Compl_subset, 
   3.210                                                  surj_Compl_image_subset]))); 
   3.211 @@ -552,13 +552,13 @@
   3.212  by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
   3.213  qed "compose_eq";
   3.214  
   3.215 -Goal "[| f : A funcset B; f `` A = B; g: B funcset C; g `` B = C |]\
   3.216 -\     ==> compose A g f `` A = C";
   3.217 +Goal "[| f : A funcset B; f ` A = B; g: B funcset C; g ` B = C |]\
   3.218 +\     ==> compose A g f ` A = C";
   3.219  by (auto_tac (claset(),
   3.220  	      simpset() addsimps [image_def, compose_eq]));
   3.221  qed "surj_compose";
   3.222  
   3.223 -Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\
   3.224 +Goal "[| f : A funcset B; g: B funcset C; f ` A = B; inj_on f A; inj_on g B |]\
   3.225  \     ==> inj_on (compose A g f) A";
   3.226  by (auto_tac (claset(),
   3.227  	      simpset() addsimps [inj_on_def, compose_eq]));
   3.228 @@ -567,7 +567,7 @@
   3.229  
   3.230  (*** restrict / lam ***)
   3.231  
   3.232 -Goal "f``A <= B ==> (lam x: A. f x) : A funcset B";
   3.233 +Goal "f`A <= B ==> (lam x: A. f x) : A funcset B";
   3.234  by (auto_tac (claset(),
   3.235  	      simpset() addsimps [restrict_def, Pi_def]));
   3.236  qed "restrict_in_funcset";
   3.237 @@ -603,17 +603,17 @@
   3.238  
   3.239  (*** Inverse ***)
   3.240  
   3.241 -Goal "[|f `` A = B;  x: B |] ==> ? y: A. f y = x";
   3.242 +Goal "[|f ` A = B;  x: B |] ==> ? y: A. f y = x";
   3.243  by (Blast_tac 1);
   3.244  qed "surj_image";
   3.245  
   3.246 -Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
   3.247 +Goalw [Inv_def] "[| f ` A = B; f : A funcset B |] \
   3.248  \                ==> (lam x: B. (Inv A f) x) : B funcset A";
   3.249  by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
   3.250  qed "Inv_funcset";
   3.251  
   3.252  
   3.253 -Goal "[| f: A funcset B;  inj_on f A;  f `` A = B;  x: A |] \
   3.254 +Goal "[| f: A funcset B;  inj_on f A;  f ` A = B;  x: A |] \
   3.255  \     ==> (lam y: B. (Inv A f) y) (f x) = x";
   3.256  by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
   3.257  by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
   3.258 @@ -621,13 +621,13 @@
   3.259  by Auto_tac;
   3.260  qed "Inv_f_f";
   3.261  
   3.262 -Goal "[| f: A funcset B;  f `` A = B;  x: B |] \
   3.263 +Goal "[| f: A funcset B;  f ` A = B;  x: B |] \
   3.264  \     ==> f ((lam y: B. (Inv A f y)) x) = x";
   3.265  by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
   3.266  by (fast_tac (claset() addIs [someI2]) 1);
   3.267  qed "f_Inv_f";
   3.268  
   3.269 -Goal "[| f: A funcset B;  inj_on f A;  f `` A = B |]\
   3.270 +Goal "[| f: A funcset B;  inj_on f A;  f ` A = B |]\
   3.271  \     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
   3.272  by (rtac Pi_extensionality 1);
   3.273  by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
     4.1 --- a/src/HOL/Inverse_Image.ML	Tue Jan 09 15:18:07 2001 +0100
     4.2 +++ b/src/HOL/Inverse_Image.ML	Tue Jan 09 15:22:13 2001 +0100
     4.3 @@ -8,32 +8,32 @@
     4.4  
     4.5  (** Basic rules **)
     4.6  
     4.7 -Goalw [vimage_def] "(a : f-``B) = (f a : B)";
     4.8 +Goalw [vimage_def] "(a : f-`B) = (f a : B)";
     4.9  by (Blast_tac 1) ;
    4.10  qed "vimage_eq";
    4.11  
    4.12  Addsimps [vimage_eq];
    4.13  
    4.14 -Goal "(a : f-``{b}) = (f a = b)";
    4.15 +Goal "(a : f-`{b}) = (f a = b)";
    4.16  by (simp_tac (simpset() addsimps [vimage_eq]) 1) ;
    4.17  qed "vimage_singleton_eq";
    4.18  
    4.19  Goalw [vimage_def]
    4.20 -    "!!A B f. [| f a = b;  b:B |] ==> a : f-``B";
    4.21 +    "!!A B f. [| f a = b;  b:B |] ==> a : f-`B";
    4.22  by (Blast_tac 1) ;
    4.23  qed "vimageI";
    4.24  
    4.25 -Goalw [vimage_def] "f a : A ==> a : f -`` A";
    4.26 +Goalw [vimage_def] "f a : A ==> a : f -` A";
    4.27  by (Fast_tac 1);
    4.28  qed "vimageI2";
    4.29  
    4.30  val major::prems = Goalw [vimage_def]
    4.31 -    "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P";
    4.32 +    "[| a: f-`B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P";
    4.33  by (rtac (major RS CollectE) 1);
    4.34  by (blast_tac (claset() addIs prems) 1) ;
    4.35  qed "vimageE";
    4.36  
    4.37 -Goalw [vimage_def] "a : f -`` A ==> f a : A";
    4.38 +Goalw [vimage_def] "a : f -` A ==> f a : A";
    4.39  by (Fast_tac 1);
    4.40  qed "vimageD";
    4.41  
    4.42 @@ -43,66 +43,66 @@
    4.43  
    4.44  (*** Equations ***)
    4.45  
    4.46 -Goal "f-``{} = {}";
    4.47 +Goal "f-`{} = {}";
    4.48  by (Blast_tac 1);
    4.49  qed "vimage_empty";
    4.50  
    4.51 -Goal "f-``(-A) = -(f-``A)";
    4.52 +Goal "f-`(-A) = -(f-`A)";
    4.53  by (Blast_tac 1);
    4.54  qed "vimage_Compl";
    4.55  
    4.56 -Goal "f-``(A Un B) = (f-``A) Un (f-``B)";
    4.57 +Goal "f-`(A Un B) = (f-`A) Un (f-`B)";
    4.58  by (Blast_tac 1);
    4.59  qed "vimage_Un";
    4.60  
    4.61 -Goal "f -`` (A Int B) = (f -`` A) Int (f -`` B)";
    4.62 +Goal "f -` (A Int B) = (f -` A) Int (f -` B)";
    4.63  by (Fast_tac 1);
    4.64  qed "vimage_Int";
    4.65  
    4.66 -Goal "f -`` (Union A) = (UN X:A. f -`` X)";
    4.67 +Goal "f -` (Union A) = (UN X:A. f -` X)";
    4.68  by (Blast_tac 1);
    4.69  qed "vimage_Union";
    4.70  
    4.71 -Goal "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
    4.72 +Goal "f-`(UN x:A. B x) = (UN x:A. f -` B x)";
    4.73  by (Blast_tac 1);
    4.74  qed "vimage_UN";
    4.75  
    4.76 -Goal "f-``(INT x:A. B x) = (INT x:A. f -`` B x)";
    4.77 +Goal "f-`(INT x:A. B x) = (INT x:A. f -` B x)";
    4.78  by (Blast_tac 1);
    4.79  qed "vimage_INT";
    4.80  
    4.81 -Goal "f -`` Collect P = {y. P (f y)}";
    4.82 +Goal "f -` Collect P = {y. P (f y)}";
    4.83  by (Blast_tac 1);
    4.84  qed "vimage_Collect_eq";
    4.85  Addsimps [vimage_Collect_eq];
    4.86  
    4.87  (*A strange result used in Tools/inductive_package*)
    4.88 -val prems = Goal "(!!x. P (f x) = Q x) ==> f -`` (Collect P) = Collect Q";
    4.89 +val prems = Goal "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q";
    4.90  by (force_tac (claset(), simpset() addsimps prems) 1);
    4.91  qed "vimage_Collect";
    4.92  
    4.93  Addsimps [vimage_empty, vimage_Un, vimage_Int];
    4.94  
    4.95  (*NOT suitable for rewriting because of the recurrence of {a}*)
    4.96 -Goal "f-``(insert a B) = (f-``{a}) Un (f-``B)";
    4.97 +Goal "f-`(insert a B) = (f-`{a}) Un (f-`B)";
    4.98  by (Blast_tac 1);
    4.99  qed "vimage_insert";
   4.100  
   4.101 -Goal "f-``(A-B) = (f-``A) - (f-``B)";
   4.102 +Goal "f-`(A-B) = (f-`A) - (f-`B)";
   4.103  by (Blast_tac 1);
   4.104  qed "vimage_Diff";
   4.105  
   4.106 -Goal "f-``UNIV = UNIV";
   4.107 +Goal "f-`UNIV = UNIV";
   4.108  by (Blast_tac 1);
   4.109  qed "vimage_UNIV";
   4.110  Addsimps [vimage_UNIV];
   4.111  
   4.112  (*NOT suitable for rewriting*)
   4.113 -Goal "f-``B = (UN y: B. f-``{y})";
   4.114 +Goal "f-`B = (UN y: B. f-`{y})";
   4.115  by (Blast_tac 1);
   4.116  qed "vimage_eq_UN";
   4.117  
   4.118  (*monotonicity*)
   4.119 -Goal "A<=B ==> f-``A <= f-``B";
   4.120 +Goal "A<=B ==> f-`A <= f-`B";
   4.121  by (Blast_tac 1);
   4.122  qed "vimage_mono";
     5.1 --- a/src/HOL/Inverse_Image.thy	Tue Jan 09 15:18:07 2001 +0100
     5.2 +++ b/src/HOL/Inverse_Image.thy	Tue Jan 09 15:22:13 2001 +0100
     5.3 @@ -9,7 +9,7 @@
     5.4  Inverse_Image = Set +
     5.5  
     5.6  constdefs
     5.7 -  vimage :: ['a => 'b, 'b set] => ('a set)   (infixr "-``" 90)
     5.8 -    "f-``B  == {x. f(x) : B}"
     5.9 +  vimage :: ['a => 'b, 'b set] => ('a set)   (infixr "-`" 90)
    5.10 +    "f-`B  == {x. f(x) : B}"
    5.11  
    5.12  end
     6.1 --- a/src/HOL/List.ML	Tue Jan 09 15:18:07 2001 +0100
     6.2 +++ b/src/HOL/List.ML	Tue Jan 09 15:22:13 2001 +0100
     6.3 @@ -448,7 +448,7 @@
     6.4  qed "set_rev";
     6.5  Addsimps [set_rev];
     6.6  
     6.7 -Goal "set(map f xs) = f``(set xs)";
     6.8 +Goal "set(map f xs) = f`(set xs)";
     6.9  by (induct_tac "xs" 1);
    6.10  by Auto_tac;
    6.11  qed "set_map";
    6.12 @@ -574,7 +574,7 @@
    6.13  qed "Nil_eq_concat_conv";
    6.14  AddIffs [Nil_eq_concat_conv];
    6.15  
    6.16 -Goal  "set(concat xs) = Union(set `` set xs)";
    6.17 +Goal  "set(concat xs) = Union(set ` set xs)";
    6.18  by (induct_tac "xs" 1);
    6.19  by Auto_tac;
    6.20  qed"set_concat";
     7.1 --- a/src/HOL/List.thy	Tue Jan 09 15:18:07 2001 +0100
     7.2 +++ b/src/HOL/List.thy	Tue Jan 09 15:22:13 2001 +0100
     7.3 @@ -177,7 +177,7 @@
     7.4   lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
     7.5  primrec
     7.6  "lexn r 0       = {}"
     7.7 -"lexn r (Suc n) = (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) `` (r <*lex*> lexn r n)) Int
     7.8 +"lexn r (Suc n) = (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
     7.9                    {(xs,ys). length xs = Suc n & length ys = Suc n}"
    7.10  
    7.11  constdefs
     8.1 --- a/src/HOL/NatDef.ML	Tue Jan 09 15:18:07 2001 +0100
     8.2 +++ b/src/HOL/NatDef.ML	Tue Jan 09 15:22:13 2001 +0100
     8.3 @@ -4,7 +4,7 @@
     8.4      Copyright   1991  University of Cambridge
     8.5  *)
     8.6  
     8.7 -Goal "mono(%X. {Zero_Rep} Un (Suc_Rep``X))";
     8.8 +Goal "mono(%X. {Zero_Rep} Un Suc_Rep`X)";
     8.9  by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
    8.10  qed "Nat_fun_mono";
    8.11  
     9.1 --- a/src/HOL/NatDef.thy	Tue Jan 09 15:18:07 2001 +0100
     9.2 +++ b/src/HOL/NatDef.thy	Tue Jan 09 15:22:13 2001 +0100
     9.3 @@ -36,7 +36,7 @@
     9.4  (* type definition *)
     9.5  
     9.6  typedef (Nat)
     9.7 -  nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"   (lfp_def)
     9.8 +  nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep`X))"   (lfp_def)
     9.9  
    9.10  instance
    9.11    nat :: {ord, zero}
    10.1 --- a/src/HOL/Product_Type.ML	Tue Jan 09 15:18:07 2001 +0100
    10.2 +++ b/src/HOL/Product_Type.ML	Tue Jan 09 15:22:13 2001 +0100
    10.3 @@ -394,14 +394,14 @@
    10.4  qed "prod_fun_ident";
    10.5  Addsimps [prod_fun_ident];
    10.6  
    10.7 -Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
    10.8 +Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)`r";
    10.9  by (rtac image_eqI 1);
   10.10  by (rtac (prod_fun RS sym) 1);
   10.11  by (assume_tac 1);
   10.12  qed "prod_fun_imageI";
   10.13  
   10.14  val major::prems = Goal
   10.15 -    "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
   10.16 +    "[| c: (prod_fun f g)`r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
   10.17  \    |] ==> P";
   10.18  by (rtac (major RS imageE) 1);
   10.19  by (res_inst_tac [("p","x")] PairE 1);
    11.1 --- a/src/HOL/Relation.ML	Tue Jan 09 15:18:07 2001 +0100
    11.2 +++ b/src/HOL/Relation.ML	Tue Jan 09 15:22:13 2001 +0100
    11.3 @@ -333,27 +333,27 @@
    11.4  
    11.5  overload_1st_set "Relation.Image";
    11.6  
    11.7 -Goalw [Image_def] "b : r```A = (? x:A. (x,b):r)";
    11.8 +Goalw [Image_def] "b : r``A = (? x:A. (x,b):r)";
    11.9  by (Blast_tac 1);
   11.10  qed "Image_iff";
   11.11  
   11.12 -Goalw [Image_def] "r```{a} = {b. (a,b):r}";
   11.13 +Goalw [Image_def] "r``{a} = {b. (a,b):r}";
   11.14  by (Blast_tac 1);
   11.15  qed "Image_singleton";
   11.16  
   11.17 -Goal "(b : r```{a}) = ((a,b):r)";
   11.18 +Goal "(b : r``{a}) = ((a,b):r)";
   11.19  by (rtac (Image_iff RS trans) 1);
   11.20  by (Blast_tac 1);
   11.21  qed "Image_singleton_iff";
   11.22  
   11.23  AddIffs [Image_singleton_iff];
   11.24  
   11.25 -Goalw [Image_def] "[| (a,b): r;  a:A |] ==> b : r```A";
   11.26 +Goalw [Image_def] "[| (a,b): r;  a:A |] ==> b : r``A";
   11.27  by (Blast_tac 1);
   11.28  qed "ImageI";
   11.29  
   11.30  val major::prems = Goalw [Image_def]
   11.31 -    "[| b: r```A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P";
   11.32 +    "[| b: r``A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P";
   11.33  by (rtac (major RS CollectE) 1);
   11.34  by (Clarify_tac 1);
   11.35  by (rtac (hd prems) 1);
   11.36 @@ -364,58 +364,58 @@
   11.37  AddSEs [ImageE];
   11.38  
   11.39  (*This version's more effective when we already have the required "a"*)
   11.40 -Goal  "[| a:A;  (a,b): r |] ==> b : r```A";
   11.41 +Goal  "[| a:A;  (a,b): r |] ==> b : r``A";
   11.42  by (Blast_tac 1);
   11.43  qed "rev_ImageI";
   11.44  
   11.45 -Goal "R```{} = {}";
   11.46 +Goal "R``{} = {}";
   11.47  by (Blast_tac 1);
   11.48  qed "Image_empty";
   11.49  
   11.50  Addsimps [Image_empty];
   11.51  
   11.52 -Goal "Id ``` A = A";
   11.53 +Goal "Id `` A = A";
   11.54  by (Blast_tac 1);
   11.55  qed "Image_Id";
   11.56  
   11.57 -Goal "diag A ``` B = A Int B";
   11.58 +Goal "diag A `` B = A Int B";
   11.59  by (Blast_tac 1);
   11.60  qed "Image_diag";
   11.61  
   11.62  Addsimps [Image_Id, Image_diag];
   11.63  
   11.64 -Goal "R ``` (A Int B) <= R ``` A Int R ``` B";
   11.65 +Goal "R `` (A Int B) <= R `` A Int R `` B";
   11.66  by (Blast_tac 1);
   11.67  qed "Image_Int_subset";
   11.68  
   11.69 -Goal "R ``` (A Un B) = R ``` A Un R ``` B";
   11.70 +Goal "R `` (A Un B) = R `` A Un R `` B";
   11.71  by (Blast_tac 1);
   11.72  qed "Image_Un";
   11.73  
   11.74 -Goal "r <= A <*> B ==> r```C <= B";
   11.75 +Goal "r <= A <*> B ==> r``C <= B";
   11.76  by (rtac subsetI 1);
   11.77  by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ;
   11.78  qed "Image_subset";
   11.79  
   11.80  (*NOT suitable for rewriting*)
   11.81 -Goal "r```B = (UN y: B. r```{y})";
   11.82 +Goal "r``B = (UN y: B. r``{y})";
   11.83  by (Blast_tac 1);
   11.84  qed "Image_eq_UN";
   11.85  
   11.86 -Goal "[| r'<=r; A'<=A |] ==> (r' ``` A') <= (r ``` A)";
   11.87 +Goal "[| r'<=r; A'<=A |] ==> (r' `` A') <= (r `` A)";
   11.88  by (Blast_tac 1);
   11.89  qed "Image_mono";
   11.90  
   11.91 -Goal "(r ``` (UNION A B)) = (UN x:A.(r ``` (B x)))";
   11.92 +Goal "(r `` (UNION A B)) = (UN x:A.(r `` (B x)))";
   11.93  by (Blast_tac 1);
   11.94  qed "Image_UN";
   11.95  
   11.96  (*Converse inclusion fails*)
   11.97 -Goal "(r ``` (INTER A B)) <= (INT x:A.(r ``` (B x)))";
   11.98 +Goal "(r `` (INTER A B)) <= (INT x:A.(r `` (B x)))";
   11.99  by (Blast_tac 1);
  11.100  qed "Image_INT_subset";
  11.101  
  11.102 -Goal "(r```A <= B) = (A <= - ((r^-1) ``` (-B)))";
  11.103 +Goal "(r``A <= B) = (A <= - ((r^-1) `` (-B)))";
  11.104  by (Blast_tac 1);
  11.105  qed "Image_subset_eq";
  11.106  
  11.107 @@ -442,7 +442,7 @@
  11.108  by Auto_tac; 
  11.109  qed "Range_Collect_split";
  11.110  
  11.111 -Goal "{(x,y). P x y} ``` A = {y. EX x:A. P x y}";
  11.112 +Goal "{(x,y). P x y} `` A = {y. EX x:A. P x y}";
  11.113  by Auto_tac; 
  11.114  qed "Image_Collect_split";
  11.115  
    12.1 --- a/src/HOL/Relation.thy	Tue Jan 09 15:18:07 2001 +0100
    12.2 +++ b/src/HOL/Relation.thy	Tue Jan 09 15:22:13 2001 +0100
    12.3 @@ -16,8 +16,8 @@
    12.4    comp  :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set"  (infixr "O" 60)
    12.5      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    12.6  
    12.7 -  Image :: "[('a*'b) set,'a set] => 'b set"                (infixl "```" 90)
    12.8 -    "r ``` s == {y. ? x:s. (x,y):r}"
    12.9 +  Image :: "[('a*'b) set,'a set] => 'b set"                (infixl "``" 90)
   12.10 +    "r `` s == {y. ? x:s. (x,y):r}"
   12.11  
   12.12    Id    :: "('a * 'a)set"                            (*the identity relation*)
   12.13      "Id == {p. ? x. p = (x,x)}"
    13.1 --- a/src/HOL/Set.ML	Tue Jan 09 15:18:07 2001 +0100
    13.2 +++ b/src/HOL/Set.ML	Tue Jan 09 15:22:13 2001 +0100
    13.3 @@ -531,7 +531,7 @@
    13.4  Addsimps [singleton_conv2];
    13.5  
    13.6  
    13.7 -section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
    13.8 +section "Unions of families -- UNION x:A. B(x) is Union(B`A)";
    13.9  
   13.10  Goalw [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))";
   13.11  by (Blast_tac 1);
   13.12 @@ -561,7 +561,7 @@
   13.13  Addcongs [UN_cong];
   13.14  
   13.15  
   13.16 -section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
   13.17 +section "Intersections of families -- INTER x:A. B(x) is Inter(B`A)";
   13.18  
   13.19  Goalw [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))";
   13.20  by Auto_tac;
   13.21 @@ -652,7 +652,7 @@
   13.22  (*** Image of a set under a function ***)
   13.23  
   13.24  (*Frequently b does not have the syntactic form of f(x).*)
   13.25 -Goalw [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
   13.26 +Goalw [image_def] "[| b=f(x);  x:A |] ==> b : f`A";
   13.27  by (Blast_tac 1);
   13.28  qed "image_eqI";
   13.29  Addsimps [image_eqI];
   13.30 @@ -660,13 +660,13 @@
   13.31  bind_thm ("imageI", refl RS image_eqI);
   13.32  
   13.33  (*This version's more effective when we already have the required x*)
   13.34 -Goalw [image_def] "[| x:A;  b=f(x) |] ==> b : f``A";
   13.35 +Goalw [image_def] "[| x:A;  b=f(x) |] ==> b : f`A";
   13.36  by (Blast_tac 1);
   13.37  qed "rev_image_eqI";
   13.38  
   13.39  (*The eta-expansion gives variable-name preservation.*)
   13.40  val major::prems = Goalw [image_def]
   13.41 -    "[| b : (%x. f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
   13.42 +    "[| b : (%x. f(x))`A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
   13.43  by (rtac (major RS CollectD RS bexE) 1);
   13.44  by (REPEAT (ares_tac prems 1));
   13.45  qed "imageE";
   13.46 @@ -674,22 +674,22 @@
   13.47  AddIs  [image_eqI];
   13.48  AddSEs [imageE]; 
   13.49  
   13.50 -Goal "f``(A Un B) = f``A Un f``B";
   13.51 +Goal "f`(A Un B) = f`A Un f`B";
   13.52  by (Blast_tac 1);
   13.53  qed "image_Un";
   13.54  
   13.55 -Goal "(z : f``A) = (EX x:A. z = f x)";
   13.56 +Goal "(z : f`A) = (EX x:A. z = f x)";
   13.57  by (Blast_tac 1);
   13.58  qed "image_iff";
   13.59  
   13.60  (*This rewrite rule would confuse users if made default.*)
   13.61 -Goal "(f``A <= B) = (ALL x:A. f(x): B)";
   13.62 +Goal "(f`A <= B) = (ALL x:A. f(x): B)";
   13.63  by (Blast_tac 1);
   13.64  qed "image_subset_iff";
   13.65  
   13.66  (*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
   13.67    many existing proofs.*)
   13.68 -val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
   13.69 +val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f`A <= B";
   13.70  by (blast_tac (claset() addIs prems) 1);
   13.71  qed "image_subsetI";
   13.72  
    14.1 --- a/src/HOL/Set.thy	Tue Jan 09 15:18:07 2001 +0100
    14.2 +++ b/src/HOL/Set.thy	Tue Jan 09 15:22:13 2001 +0100
    14.3 @@ -34,7 +34,7 @@
    14.4    Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
    14.5    Pow           :: 'a set => 'a set set                 (*powerset*)
    14.6    Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
    14.7 -  "image"       :: ['a => 'b, 'a set] => ('b set)   (infixr "``" 90)
    14.8 +  "image"       :: ['a => 'b, 'a set] => ('b set)   (infixr "`" 90)
    14.9    (*membership*)
   14.10    "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
   14.11  
   14.12 @@ -70,7 +70,7 @@
   14.13    "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
   14.14  
   14.15  translations
   14.16 -  "range f"     == "f``UNIV"
   14.17 +  "range f"     == "f`UNIV"
   14.18    "x ~: y"      == "~ (x : y)"
   14.19    "{x, xs}"     == "insert x {xs}"
   14.20    "{x}"         == "insert x {}"
   14.21 @@ -145,7 +145,7 @@
   14.22    empty_def     "{}             == {x. False}"
   14.23    UNIV_def      "UNIV           == {x. True}"
   14.24    insert_def    "insert a B     == {x. x=a} Un B"
   14.25 -  image_def     "f``A           == {y. ? x:A. y=f(x)}"
   14.26 +  image_def     "f`A           == {y. ? x:A. y=f(x)}"
   14.27  
   14.28  
   14.29  end
    15.1 --- a/src/HOL/Sum_Type.thy	Tue Jan 09 15:18:07 2001 +0100
    15.2 +++ b/src/HOL/Sum_Type.thy	Tue Jan 09 15:22:13 2001 +0100
    15.3 @@ -40,7 +40,7 @@
    15.4    Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
    15.5    Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
    15.6  
    15.7 -  sum_def       "A <+> B == (Inl``A) Un (Inr``B)"
    15.8 +  sum_def       "A <+> B == (Inl`A) Un (Inr`B)"
    15.9  
   15.10    (*for selecting out the components of a mutually recursive definition*)
   15.11    Part_def      "Part A h == A Int {x. ? z. x = h(z)}"
    16.1 --- a/src/HOL/Wellfounded_Recursion.ML	Tue Jan 09 15:18:07 2001 +0100
    16.2 +++ b/src/HOL/Wellfounded_Recursion.ML	Tue Jan 09 15:22:13 2001 +0100
    16.3 @@ -193,7 +193,7 @@
    16.4   * Wellfoundedness of `image'
    16.5   *---------------------------------------------------------------------------*)
    16.6  
    16.7 -Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)";
    16.8 +Goal "[| wf r; inj f |] ==> wf(prod_fun f f ` r)";
    16.9  by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
   16.10  by (Clarify_tac 1);
   16.11  by (case_tac "EX p. f p : Q" 1);
    17.1 --- a/src/HOL/equalities.ML	Tue Jan 09 15:18:07 2001 +0100
    17.2 +++ b/src/HOL/equalities.ML	Tue Jan 09 15:22:13 2001 +0100
    17.3 @@ -112,49 +112,49 @@
    17.4  by (Blast_tac 1);
    17.5  qed "UN_insert_distrib";
    17.6  
    17.7 -section "``";
    17.8 +section "`";
    17.9  
   17.10 -Goal "f``{} = {}";
   17.11 +Goal "f`{} = {}";
   17.12  by (Blast_tac 1);
   17.13  qed "image_empty";
   17.14  Addsimps[image_empty];
   17.15  
   17.16 -Goal "f``insert a B = insert (f a) (f``B)";
   17.17 +Goal "f`insert a B = insert (f a) (f`B)";
   17.18  by (Blast_tac 1);
   17.19  qed "image_insert";
   17.20  Addsimps[image_insert];
   17.21  
   17.22 -Goal "x:A ==> (%x. c) `` A = {c}";
   17.23 +Goal "x:A ==> (%x. c) ` A = {c}";
   17.24  by (Blast_tac 1);
   17.25  qed "image_constant";
   17.26  
   17.27 -Goal "f``(g``A) = (%x. f (g x)) `` A";
   17.28 +Goal "f`(g`A) = (%x. f (g x)) ` A";
   17.29  by (Blast_tac 1);
   17.30  qed "image_image";
   17.31  
   17.32 -Goal "x:A ==> insert (f x) (f``A) = f``A";
   17.33 +Goal "x:A ==> insert (f x) (f`A) = f`A";
   17.34  by (Blast_tac 1);
   17.35  qed "insert_image";
   17.36  Addsimps [insert_image];
   17.37  
   17.38 -Goal "(f``A = {}) = (A = {})";
   17.39 +Goal "(f`A = {}) = (A = {})";
   17.40  by (blast_tac (claset() addSEs [equalityCE]) 1);
   17.41  qed "image_is_empty";
   17.42  AddIffs [image_is_empty];
   17.43  
   17.44 -Goal "f `` {x. P x} = {f x | x. P x}";
   17.45 +Goal "f ` {x. P x} = {f x | x. P x}";
   17.46  by (Blast_tac 1);
   17.47  qed "image_Collect";
   17.48  Addsimps [image_Collect];
   17.49  
   17.50 -Goalw [image_def] "(%x. if P x then f x else g x) `` S   \
   17.51 -\                = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";
   17.52 +Goalw [image_def] "(%x. if P x then f x else g x) ` S   \
   17.53 +\                = (f ` (S Int {x. P x})) Un (g ` (S Int {x. ~(P x)}))";
   17.54  by (Simp_tac 1);
   17.55  by (Blast_tac 1);
   17.56  qed "if_image_distrib";
   17.57  Addsimps[if_image_distrib];
   17.58  
   17.59 -val prems = Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
   17.60 +val prems = Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f`M = g`N";
   17.61  by (simp_tac (simpset() addsimps image_def::prems) 1);
   17.62  qed "image_cong";
   17.63  
   17.64 @@ -165,7 +165,7 @@
   17.65  by Auto_tac;
   17.66  qed "full_SetCompr_eq";
   17.67  
   17.68 -Goal "range (%x. f (g x)) = f``range g";
   17.69 +Goal "range (%x. f (g x)) = f`range g";
   17.70  by (stac image_image 1);
   17.71  by (Simp_tac 1);
   17.72  qed "range_composition";
   17.73 @@ -563,16 +563,16 @@
   17.74  by (Blast_tac 1);
   17.75  qed "INT_insert_distrib";
   17.76  
   17.77 -Goal "Union(B``A) = (UN x:A. B(x))";
   17.78 +Goal "Union(B`A) = (UN x:A. B(x))";
   17.79  by (Blast_tac 1);
   17.80  qed "Union_image_eq";
   17.81  Addsimps [Union_image_eq];
   17.82  
   17.83 -Goal "f `` Union S = (UN x:S. f `` x)";
   17.84 +Goal "f ` Union S = (UN x:S. f ` x)";
   17.85  by (Blast_tac 1);
   17.86  qed "image_Union";
   17.87  
   17.88 -Goal "Inter(B``A) = (INT x:A. B(x))";
   17.89 +Goal "Inter(B`A) = (INT x:A. B(x))";
   17.90  by (Blast_tac 1);
   17.91  qed "Inter_image_eq";
   17.92  Addsimps [Inter_image_eq];
   17.93 @@ -614,7 +614,7 @@
   17.94  
   17.95  (* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
   17.96     Union of a family of unions **)
   17.97 -Goal "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
   17.98 +Goal "(UN x:C. A(x) Un B(x)) = Union(A`C)  Un  Union(B`C)";
   17.99  by (Blast_tac 1);
  17.100  qed "Un_Union_image";
  17.101  
  17.102 @@ -627,7 +627,7 @@
  17.103  by (Blast_tac 1);
  17.104  qed "Un_Inter";
  17.105  
  17.106 -Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
  17.107 +Goal "(INT x:C. A(x) Int B(x)) = Inter(A`C) Int Inter(B`C)";
  17.108  by (Blast_tac 1);
  17.109  qed "Int_Inter_image";
  17.110  
  17.111 @@ -842,7 +842,7 @@
  17.112  qed "Pow_empty";
  17.113  Addsimps [Pow_empty];
  17.114  
  17.115 -Goal "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
  17.116 +Goal "Pow (insert a A) = Pow A Un (insert a ` Pow A)";
  17.117  by (blast_tac (claset() addIs [inst "x" "?u-{a}" image_eqI]) 1);
  17.118  qed "Pow_insert";
  17.119  
  17.120 @@ -922,7 +922,7 @@
  17.121       "(UN x:C. A - B x)    = (A - (INT x:C. B x))",
  17.122       "(UN x: Union A. B x) = (UN y:A. UN x:y. B x)",
  17.123       "(UN z: UNION A B. C z) = (UN  x:A. UN z: B(x). C z)",
  17.124 -     "(UN x:f``A. B x)     = (UN a:A. B(f a))"];
  17.125 +     "(UN x:f`A. B x)     = (UN a:A. B(f a))"];
  17.126  
  17.127  val INT_simps = map prover
  17.128      ["!!C. c: C ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
  17.129 @@ -934,7 +934,7 @@
  17.130       "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))",
  17.131       "(INT x: Union A. B x) = (INT y:A. INT x:y. B x)",
  17.132       "(INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)",
  17.133 -     "(INT x:f``A. B x)    = (INT a:A. B(f a))"];
  17.134 +     "(INT x:f`A. B x)    = (INT a:A. B(f a))"];
  17.135  
  17.136  
  17.137  val ball_simps = map prover
  17.138 @@ -948,7 +948,7 @@
  17.139       "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
  17.140       "(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)",
  17.141       "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",
  17.142 -     "(ALL x:f``A. P x) = (ALL x:A. P(f x))",
  17.143 +     "(ALL x:f`A. P x) = (ALL x:A. P(f x))",
  17.144       "(~(ALL x:A. P x)) = (EX x:A. ~P x)"];
  17.145  
  17.146  val ball_conj_distrib = 
  17.147 @@ -963,7 +963,7 @@
  17.148       "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
  17.149       "(EX x: UNION A B. P x) = (EX a:A. EX x: B a.  P x)",
  17.150       "(EX x:Collect Q. P x) = (EX x. Q x & P x)",
  17.151 -     "(EX x:f``A. P x) = (EX x:A. P(f x))",
  17.152 +     "(EX x:f`A. P x) = (EX x:A. P(f x))",
  17.153       "(~(EX x:A. P x)) = (ALL x:A. ~P x)"];
  17.154  
  17.155  val bex_disj_distrib = 
    18.1 --- a/src/HOL/mono.ML	Tue Jan 09 15:18:07 2001 +0100
    18.2 +++ b/src/HOL/mono.ML	Tue Jan 09 15:22:13 2001 +0100
    18.3 @@ -6,7 +6,7 @@
    18.4  Monotonicity of various operations
    18.5  *)
    18.6  
    18.7 -Goal "A<=B ==> f``A <= f``B";
    18.8 +Goal "A<=B ==> f`A <= f`B";
    18.9  by (Blast_tac 1);
   18.10  qed "image_mono";
   18.11  
   18.12 @@ -107,7 +107,7 @@
   18.13  (* Courtesy of Stephan Merz *)
   18.14  Goalw [Least_def,mono_def]
   18.15    "[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \
   18.16 -\  ==> (LEAST y. y : f``S) = f(LEAST x. x : S)";
   18.17 +\  ==> (LEAST y. y : f`S) = f(LEAST x. x : S)";
   18.18  by (etac bexE 1);
   18.19  by (rtac someI2 1);
   18.20  by (Force_tac 1);