# HG changeset patch
# User nipkow
# Date 979050133 -3600
# Node ID e33b47e4246d9903cadd57c1afaf662343026eed
# Parent  024bdf8e52a4f2f7c929d3996dc4973f29ec510b
`` ->  and ``` -> ``

diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Datatype_Universe.thy
--- a/src/HOL/Datatype_Universe.thy	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Datatype_Universe.thy	Tue Jan 09 15:22:13 2001 +0100
@@ -63,7 +63,7 @@
 
   (*S-expression constructors*)
   Atom_def   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
-  Scons_def  "Scons M N == (Push_Node (Inr 1) `` M) Un (Push_Node (Inr 2) `` N)"
+  Scons_def  "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr 2) ` N)"
 
   (*Leaf nodes, with arbitrary or nat labels*)
   Leaf_def   "Leaf == Atom o Inl"
@@ -74,7 +74,7 @@
   In1_def    "In1(M) == Scons (Numb 1) M"
 
   (*Function spaces*)
-  Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) `` (f x)}"
+  Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}"
   Funs_def "Funs S == {f. range f <= S}"
 
   (*the set of nodes with depth less than k*)
@@ -83,7 +83,7 @@
 
   (*products and sums for the "universe"*)
   uprod_def  "uprod A B == UN x:A. UN y:B. { Scons x y }"
-  usum_def   "usum A B == In0``A Un In1``B"
+  usum_def   "usum A B == In0`A Un In1`B"
 
   (*the corresponding eliminators*)
   Split_def  "Split c M == @u. ? x y. M = Scons x y & u = c x y"
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Finite.ML	Tue Jan 09 15:22:13 2001 +0100
@@ -74,7 +74,7 @@
 Addsimps[finite_insert];
 
 (*The image of a finite set is finite *)
-Goal  "finite F ==> finite(h``F)";
+Goal  "finite F ==> finite(h`F)";
 by (etac finite_induct 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
@@ -127,11 +127,11 @@
 val lemma = result();
 
 (*Lemma for proving finite_imageD*)
-Goal "finite B ==> ALL A. f``A = B --> inj_on f A --> finite A";
+Goal "finite B ==> ALL A. f`A = B --> inj_on f A --> finite A";
 by (etac finite_induct 1);
  by (ALLGOALS Asm_simp_tac);
 by (Clarify_tac 1);
-by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
+by (subgoal_tac "EX y:A. f y = x & F = f`(A-{y})" 1);
  by (Clarify_tac 1);
  by (full_simp_tac (simpset() addsimps [inj_on_def]) 1);
  by (blast_tac (claset() addSDs [lemma RS iffD1]) 1);
@@ -143,7 +143,7 @@
     (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff])));
 val lemma = result();
 
-Goal "[| finite(f``A);  inj_on f A |] ==> finite A";
+Goal "[| finite(f`A);  inj_on f A |] ==> finite A";
 by (dtac lemma 1);
 by (Blast_tac 1);
 qed "finite_imageD";
@@ -195,7 +195,7 @@
 (** The powerset of a finite set **)
 
 Goal "finite(Pow A) ==> finite A";
-by (subgoal_tac "finite ((%x.{x})``A)" 1);
+by (subgoal_tac "finite ((%x.{x})`A)" 1);
 by (rtac finite_subset 2);
 by (assume_tac 3);
 by (ALLGOALS
@@ -214,7 +214,7 @@
 AddIffs [finite_Pow_iff];
 
 Goal "finite(r^-1) = finite r";
-by (subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
+by (subgoal_tac "r^-1 = (%(x,y).(y,x))`r" 1);
  by (Asm_simp_tac 1);
  by (rtac iffI 1);
   by (etac (rewrite_rule [inj_on_def] finite_imageD) 1);
@@ -467,14 +467,14 @@
 
 (*** Cardinality of image ***)
 
-Goal "finite A ==> card (f `` A) <= card A";
+Goal "finite A ==> card (f ` A) <= card A";
 by (etac finite_induct 1);
  by (Simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [le_SucI, finite_imageI, 
 				      card_insert_if]) 1);
 qed "card_image_le";
 
-Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A";
+Goal "finite(A) ==> inj_on f A --> card (f ` A) = card A";
 by (etac finite_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by Safe_tac;
@@ -486,7 +486,7 @@
 by (Blast_tac 1);
 qed_spec_mp "card_image";
 
-Goal "[| finite A; f``A <= A; inj_on f A |] ==> f``A = A";
+Goal "[| finite A; f`A <= A; inj_on f A |] ==> f`A = A";
 by (asm_simp_tac (simpset() addsimps [card_seteq, card_image]) 1);
 qed "endo_inj_surj";
 
@@ -853,14 +853,14 @@
 by (auto_tac (claset() addIs [finite_subset], simpset()));
 qed "choose_deconstruct";
 
-Goal "[| finite(A); finite(B);  f``A <= B;  inj_on f A |] \
+Goal "[| finite(A); finite(B);  f`A <= B;  inj_on f A |] \
 \     ==> card A <= card B";
 by (auto_tac (claset() addIs [card_mono], 
 	      simpset() addsimps [card_image RS sym]));
 qed "card_inj_on_le";
 
 Goal "[| finite A; finite B; \
-\        f``A <= B; inj_on f A; g``B <= A; inj_on g B |] \
+\        f`A <= B; inj_on f A; g`B <= A; inj_on g B |] \
 \     ==> card(A) = card(B)";
 by (auto_tac (claset() addIs [le_anti_sym,card_inj_on_le], simpset()));
 qed "card_bij_eq";
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Fun.ML	Tue Jan 09 15:22:13 2001 +0100
@@ -65,15 +65,15 @@
 qed "o_id";
 Addsimps [o_id];
 
-Goalw [o_def] "(f o g)``r = f``(g``r)";
+Goalw [o_def] "(f o g)`r = f`(g`r)";
 by (Blast_tac 1);
 qed "image_compose";
 
-Goal "f``A = (UN x:A. {f x})";
+Goal "f`A = (UN x:A. {f x})";
 by (Blast_tac 1);
 qed "image_eq_UN";
 
-Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
+Goalw [o_def] "UNION A (g o f) = UNION (f`A) g";
 by (Blast_tac 1);
 qed "UN_o";
 
@@ -205,7 +205,7 @@
 
 (*** Lemmas about injective functions and inv ***)
 
-Goalw [o_def] "[| inj_on f A;  inj_on g (f``A) |] ==> inj_on (g o f) A";
+Goalw [o_def] "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A";
 by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
 qed "comp_inj_on";
 
@@ -288,147 +288,147 @@
 (** We seem to need both the id-forms and the (%x. x) forms; the latter can
     arise by rewriting, while id may be used explicitly. **)
 
-Goal "(%x. x) `` Y = Y";
+Goal "(%x. x) ` Y = Y";
 by (Blast_tac 1);
 qed "image_ident";
 
-Goalw [id_def] "id `` Y = Y";
+Goalw [id_def] "id ` Y = Y";
 by (Blast_tac 1);
 qed "image_id";
 Addsimps [image_ident, image_id];
 
-Goal "(%x. x) -`` Y = Y";
+Goal "(%x. x) -` Y = Y";
 by (Blast_tac 1);
 qed "vimage_ident";
 
-Goalw [id_def] "id -`` A = A";
+Goalw [id_def] "id -` A = A";
 by Auto_tac;
 qed "vimage_id";
 Addsimps [vimage_ident, vimage_id];
 
-Goal "f -`` (f `` A) = {y. EX x:A. f x = f y}";
+Goal "f -` (f ` A) = {y. EX x:A. f x = f y}";
 by (blast_tac (claset() addIs [sym]) 1);
 qed "vimage_image_eq";
 
-Goal "f `` (f -`` A) <= A";
+Goal "f ` (f -` A) <= A";
 by (Blast_tac 1);
 qed "image_vimage_subset";
 
-Goal "f `` (f -`` A) = A Int range f";
+Goal "f ` (f -` A) = A Int range f";
 by (Blast_tac 1);
 qed "image_vimage_eq";
 Addsimps [image_vimage_eq];
 
-Goal "surj f ==> f `` (f -`` A) = A";
+Goal "surj f ==> f ` (f -` A) = A";
 by (asm_simp_tac (simpset() addsimps [surj_range]) 1);
 qed "surj_image_vimage_eq";
 
-Goal "surj f ==> f `` (inv f `` A) = A";
+Goal "surj f ==> f ` (inv f ` A) = A";
 by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1);
 qed "image_surj_f_inv_f";
 
-Goalw [inj_on_def] "inj f ==> f -`` (f `` A) = A";
+Goalw [inj_on_def] "inj f ==> f -` (f ` A) = A";
 by (Blast_tac 1);
 qed "inj_vimage_image_eq";
 
-Goal "inj f ==> (inv f) `` (f `` A) = A";
+Goal "inj f ==> (inv f) ` (f ` A) = A";
 by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1);
 qed "image_inv_f_f";
 
-Goalw [surj_def] "surj f ==> f -`` B <= A ==> B <= f `` A";
+Goalw [surj_def] "surj f ==> f -` B <= A ==> B <= f ` A";
 by (blast_tac (claset() addIs [sym]) 1);
 qed "vimage_subsetD";
 
-Goalw [inj_on_def] "inj f ==> B <= f `` A ==> f -`` B <= A";
+Goalw [inj_on_def] "inj f ==> B <= f ` A ==> f -` B <= A";
 by (Blast_tac 1);
 qed "vimage_subsetI";
 
-Goalw [bij_def] "bij f ==> (f -`` B <= A) = (B <= f `` A)";
+Goalw [bij_def] "bij f ==> (f -` B <= A) = (B <= f ` A)";
 by (blast_tac (claset() delrules [subsetI]
 			addIs [vimage_subsetI, vimage_subsetD]) 1);
 qed "vimage_subset_eq";
 
-Goal "f``(A Int B) <= f``A Int f``B";
+Goal "f`(A Int B) <= f`A Int f`B";
 by (Blast_tac 1);
 qed "image_Int_subset";
 
-Goal "f``A - f``B <= f``(A - B)";
+Goal "f`A - f`B <= f`(A - B)";
 by (Blast_tac 1);
 qed "image_diff_subset";
 
 Goalw [inj_on_def]
-   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
+   "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A Int B) = f`A Int f`B";
 by (Blast_tac 1);
 qed "inj_on_image_Int";
 
 Goalw [inj_on_def]
-   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
+   "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A-B) = f`A - f`B";
 by (Blast_tac 1);
 qed "inj_on_image_set_diff";
 
-Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B";
+Goalw [inj_on_def] "inj f ==> f`(A Int B) = f`A Int f`B";
 by (Blast_tac 1);
 qed "image_Int";
 
-Goalw [inj_on_def] "inj f ==> f``(A-B) = f``A - f``B";
+Goalw [inj_on_def] "inj f ==> f`(A-B) = f`A - f`B";
 by (Blast_tac 1);
 qed "image_set_diff";
 
-Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X";
+Goalw [image_def] "inj(f) ==> inv(f)`(f`X) = X";
 by Auto_tac;
 qed "inv_image_comp";
 
-Goal "inj f ==> (f a : f``A) = (a : A)";
+Goal "inj f ==> (f a : f`A) = (a : A)";
 by (blast_tac (claset() addDs [injD]) 1);
 qed "inj_image_mem_iff";
 
-Goalw [inj_on_def] "inj f ==> (f``A <= f``B) = (A<=B)";
+Goalw [inj_on_def] "inj f ==> (f`A <= f`B) = (A<=B)";
 by (Blast_tac 1);
 qed "inj_image_subset_iff";
 
-Goal "inj f ==> (f``A = f``B) = (A = B)";
+Goal "inj f ==> (f`A = f`B) = (A = B)";
 by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
 qed "inj_image_eq_iff";
 
-Goal  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
+Goal  "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))";
 by (Blast_tac 1);
 qed "image_UN";
 
 (*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
 Goalw [inj_on_def]
    "[| inj_on f C;  ALL x:A. B x <= C;  j:A |] \
-\   ==> f `` (INTER A B) = (INT x:A. f `` B x)";
+\   ==> f ` (INTER A B) = (INT x:A. f ` B x)";
 by (Blast_tac 1);
 qed "image_INT";
 
 (*Compare with image_INT: no use of inj_on, and if f is surjective then
   it doesn't matter whether A is empty*)
-Goalw [bij_def] "bij f ==> f `` (INTER A B) = (INT x:A. f `` B x)";
+Goalw [bij_def] "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)";
 by (force_tac (claset() addSIs [surj_f_inv_f RS sym RS image_eqI], 
 	       simpset()) 1);
 qed "bij_image_INT";
 
-Goal "bij f ==> f `` Collect P = {y. P (inv f y)}";
+Goal "bij f ==> f ` Collect P = {y. P (inv f y)}";
 by Auto_tac;
 by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1);
 by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1);
 qed "bij_image_Collect_eq";
 
-Goal "bij f ==> f -`` A = inv f `` A";
+Goal "bij f ==> f -` A = inv f ` A";
 by Safe_tac;
 by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
 by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
 qed "bij_vimage_eq_inv_image";
 
-Goal "surj f ==> -(f``A) <= f``(-A)";
+Goal "surj f ==> -(f`A) <= f`(-A)";
 by (auto_tac (claset(), simpset() addsimps [surj_def]));  
 qed "surj_Compl_image_subset";
 
-Goal "inj f ==> f``(-A) <= -(f``A)";
+Goal "inj f ==> f`(-A) <= -(f`A)";
 by (auto_tac (claset(), simpset() addsimps [inj_on_def]));  
 qed "inj_image_Compl_subset";
 
-Goalw [bij_def] "bij f ==> f``(-A) = -(f``A)";
+Goalw [bij_def] "bij f ==> f`(-A) = -(f`A)";
 by (rtac equalityI 1); 
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [inj_image_Compl_subset, 
                                                 surj_Compl_image_subset]))); 
@@ -552,13 +552,13 @@
 by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
 qed "compose_eq";
 
-Goal "[| f : A funcset B; f `` A = B; g: B funcset C; g `` B = C |]\
-\     ==> compose A g f `` A = C";
+Goal "[| f : A funcset B; f ` A = B; g: B funcset C; g ` B = C |]\
+\     ==> compose A g f ` A = C";
 by (auto_tac (claset(),
 	      simpset() addsimps [image_def, compose_eq]));
 qed "surj_compose";
 
-Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\
+Goal "[| f : A funcset B; g: B funcset C; f ` A = B; inj_on f A; inj_on g B |]\
 \     ==> inj_on (compose A g f) A";
 by (auto_tac (claset(),
 	      simpset() addsimps [inj_on_def, compose_eq]));
@@ -567,7 +567,7 @@
 
 (*** restrict / lam ***)
 
-Goal "f``A <= B ==> (lam x: A. f x) : A funcset B";
+Goal "f`A <= B ==> (lam x: A. f x) : A funcset B";
 by (auto_tac (claset(),
 	      simpset() addsimps [restrict_def, Pi_def]));
 qed "restrict_in_funcset";
@@ -603,17 +603,17 @@
 
 (*** Inverse ***)
 
-Goal "[|f `` A = B;  x: B |] ==> ? y: A. f y = x";
+Goal "[|f ` A = B;  x: B |] ==> ? y: A. f y = x";
 by (Blast_tac 1);
 qed "surj_image";
 
-Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
+Goalw [Inv_def] "[| f ` A = B; f : A funcset B |] \
 \                ==> (lam x: B. (Inv A f) x) : B funcset A";
 by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
 qed "Inv_funcset";
 
 
-Goal "[| f: A funcset B;  inj_on f A;  f `` A = B;  x: A |] \
+Goal "[| f: A funcset B;  inj_on f A;  f ` A = B;  x: A |] \
 \     ==> (lam y: B. (Inv A f) y) (f x) = x";
 by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
 by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
@@ -621,13 +621,13 @@
 by Auto_tac;
 qed "Inv_f_f";
 
-Goal "[| f: A funcset B;  f `` A = B;  x: B |] \
+Goal "[| f: A funcset B;  f ` A = B;  x: B |] \
 \     ==> f ((lam y: B. (Inv A f y)) x) = x";
 by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
 by (fast_tac (claset() addIs [someI2]) 1);
 qed "f_Inv_f";
 
-Goal "[| f: A funcset B;  inj_on f A;  f `` A = B |]\
+Goal "[| f: A funcset B;  inj_on f A;  f ` A = B |]\
 \     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
 by (rtac Pi_extensionality 1);
 by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Inverse_Image.ML
--- a/src/HOL/Inverse_Image.ML	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Inverse_Image.ML	Tue Jan 09 15:22:13 2001 +0100
@@ -8,32 +8,32 @@
 
 (** Basic rules **)
 
-Goalw [vimage_def] "(a : f-``B) = (f a : B)";
+Goalw [vimage_def] "(a : f-`B) = (f a : B)";
 by (Blast_tac 1) ;
 qed "vimage_eq";
 
 Addsimps [vimage_eq];
 
-Goal "(a : f-``{b}) = (f a = b)";
+Goal "(a : f-`{b}) = (f a = b)";
 by (simp_tac (simpset() addsimps [vimage_eq]) 1) ;
 qed "vimage_singleton_eq";
 
 Goalw [vimage_def]
-    "!!A B f. [| f a = b;  b:B |] ==> a : f-``B";
+    "!!A B f. [| f a = b;  b:B |] ==> a : f-`B";
 by (Blast_tac 1) ;
 qed "vimageI";
 
-Goalw [vimage_def] "f a : A ==> a : f -`` A";
+Goalw [vimage_def] "f a : A ==> a : f -` A";
 by (Fast_tac 1);
 qed "vimageI2";
 
 val major::prems = Goalw [vimage_def]
-    "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P";
+    "[| a: f-`B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P";
 by (rtac (major RS CollectE) 1);
 by (blast_tac (claset() addIs prems) 1) ;
 qed "vimageE";
 
-Goalw [vimage_def] "a : f -`` A ==> f a : A";
+Goalw [vimage_def] "a : f -` A ==> f a : A";
 by (Fast_tac 1);
 qed "vimageD";
 
@@ -43,66 +43,66 @@
 
 (*** Equations ***)
 
-Goal "f-``{} = {}";
+Goal "f-`{} = {}";
 by (Blast_tac 1);
 qed "vimage_empty";
 
-Goal "f-``(-A) = -(f-``A)";
+Goal "f-`(-A) = -(f-`A)";
 by (Blast_tac 1);
 qed "vimage_Compl";
 
-Goal "f-``(A Un B) = (f-``A) Un (f-``B)";
+Goal "f-`(A Un B) = (f-`A) Un (f-`B)";
 by (Blast_tac 1);
 qed "vimage_Un";
 
-Goal "f -`` (A Int B) = (f -`` A) Int (f -`` B)";
+Goal "f -` (A Int B) = (f -` A) Int (f -` B)";
 by (Fast_tac 1);
 qed "vimage_Int";
 
-Goal "f -`` (Union A) = (UN X:A. f -`` X)";
+Goal "f -` (Union A) = (UN X:A. f -` X)";
 by (Blast_tac 1);
 qed "vimage_Union";
 
-Goal "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
+Goal "f-`(UN x:A. B x) = (UN x:A. f -` B x)";
 by (Blast_tac 1);
 qed "vimage_UN";
 
-Goal "f-``(INT x:A. B x) = (INT x:A. f -`` B x)";
+Goal "f-`(INT x:A. B x) = (INT x:A. f -` B x)";
 by (Blast_tac 1);
 qed "vimage_INT";
 
-Goal "f -`` Collect P = {y. P (f y)}";
+Goal "f -` Collect P = {y. P (f y)}";
 by (Blast_tac 1);
 qed "vimage_Collect_eq";
 Addsimps [vimage_Collect_eq];
 
 (*A strange result used in Tools/inductive_package*)
-val prems = Goal "(!!x. P (f x) = Q x) ==> f -`` (Collect P) = Collect Q";
+val prems = Goal "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q";
 by (force_tac (claset(), simpset() addsimps prems) 1);
 qed "vimage_Collect";
 
 Addsimps [vimage_empty, vimage_Un, vimage_Int];
 
 (*NOT suitable for rewriting because of the recurrence of {a}*)
-Goal "f-``(insert a B) = (f-``{a}) Un (f-``B)";
+Goal "f-`(insert a B) = (f-`{a}) Un (f-`B)";
 by (Blast_tac 1);
 qed "vimage_insert";
 
-Goal "f-``(A-B) = (f-``A) - (f-``B)";
+Goal "f-`(A-B) = (f-`A) - (f-`B)";
 by (Blast_tac 1);
 qed "vimage_Diff";
 
-Goal "f-``UNIV = UNIV";
+Goal "f-`UNIV = UNIV";
 by (Blast_tac 1);
 qed "vimage_UNIV";
 Addsimps [vimage_UNIV];
 
 (*NOT suitable for rewriting*)
-Goal "f-``B = (UN y: B. f-``{y})";
+Goal "f-`B = (UN y: B. f-`{y})";
 by (Blast_tac 1);
 qed "vimage_eq_UN";
 
 (*monotonicity*)
-Goal "A<=B ==> f-``A <= f-``B";
+Goal "A<=B ==> f-`A <= f-`B";
 by (Blast_tac 1);
 qed "vimage_mono";
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Inverse_Image.thy
--- a/src/HOL/Inverse_Image.thy	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Inverse_Image.thy	Tue Jan 09 15:22:13 2001 +0100
@@ -9,7 +9,7 @@
 Inverse_Image = Set +
 
 constdefs
-  vimage :: ['a => 'b, 'b set] => ('a set)   (infixr "-``" 90)
-    "f-``B  == {x. f(x) : B}"
+  vimage :: ['a => 'b, 'b set] => ('a set)   (infixr "-`" 90)
+    "f-`B  == {x. f(x) : B}"
 
 end
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/List.ML
--- a/src/HOL/List.ML	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/List.ML	Tue Jan 09 15:22:13 2001 +0100
@@ -448,7 +448,7 @@
 qed "set_rev";
 Addsimps [set_rev];
 
-Goal "set(map f xs) = f``(set xs)";
+Goal "set(map f xs) = f`(set xs)";
 by (induct_tac "xs" 1);
 by Auto_tac;
 qed "set_map";
@@ -574,7 +574,7 @@
 qed "Nil_eq_concat_conv";
 AddIffs [Nil_eq_concat_conv];
 
-Goal  "set(concat xs) = Union(set `` set xs)";
+Goal  "set(concat xs) = Union(set ` set xs)";
 by (induct_tac "xs" 1);
 by Auto_tac;
 qed"set_concat";
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/List.thy	Tue Jan 09 15:22:13 2001 +0100
@@ -177,7 +177,7 @@
  lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
 primrec
 "lexn r 0       = {}"
-"lexn r (Suc n) = (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) `` (r <*lex*> lexn r n)) Int
+"lexn r (Suc n) = (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
                   {(xs,ys). length xs = Suc n & length ys = Suc n}"
 
 constdefs
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/NatDef.ML	Tue Jan 09 15:22:13 2001 +0100
@@ -4,7 +4,7 @@
     Copyright   1991  University of Cambridge
 *)
 
-Goal "mono(%X. {Zero_Rep} Un (Suc_Rep``X))";
+Goal "mono(%X. {Zero_Rep} Un Suc_Rep`X)";
 by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
 qed "Nat_fun_mono";
 
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/NatDef.thy
--- a/src/HOL/NatDef.thy	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/NatDef.thy	Tue Jan 09 15:22:13 2001 +0100
@@ -36,7 +36,7 @@
 (* type definition *)
 
 typedef (Nat)
-  nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"   (lfp_def)
+  nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep`X))"   (lfp_def)
 
 instance
   nat :: {ord, zero}
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Product_Type.ML
--- a/src/HOL/Product_Type.ML	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Product_Type.ML	Tue Jan 09 15:22:13 2001 +0100
@@ -394,14 +394,14 @@
 qed "prod_fun_ident";
 Addsimps [prod_fun_ident];
 
-Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
+Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)`r";
 by (rtac image_eqI 1);
 by (rtac (prod_fun RS sym) 1);
 by (assume_tac 1);
 qed "prod_fun_imageI";
 
 val major::prems = Goal
-    "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
+    "[| c: (prod_fun f g)`r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
 \    |] ==> P";
 by (rtac (major RS imageE) 1);
 by (res_inst_tac [("p","x")] PairE 1);
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Relation.ML	Tue Jan 09 15:22:13 2001 +0100
@@ -333,27 +333,27 @@
 
 overload_1st_set "Relation.Image";
 
-Goalw [Image_def] "b : r```A = (? x:A. (x,b):r)";
+Goalw [Image_def] "b : r``A = (? x:A. (x,b):r)";
 by (Blast_tac 1);
 qed "Image_iff";
 
-Goalw [Image_def] "r```{a} = {b. (a,b):r}";
+Goalw [Image_def] "r``{a} = {b. (a,b):r}";
 by (Blast_tac 1);
 qed "Image_singleton";
 
-Goal "(b : r```{a}) = ((a,b):r)";
+Goal "(b : r``{a}) = ((a,b):r)";
 by (rtac (Image_iff RS trans) 1);
 by (Blast_tac 1);
 qed "Image_singleton_iff";
 
 AddIffs [Image_singleton_iff];
 
-Goalw [Image_def] "[| (a,b): r;  a:A |] ==> b : r```A";
+Goalw [Image_def] "[| (a,b): r;  a:A |] ==> b : r``A";
 by (Blast_tac 1);
 qed "ImageI";
 
 val major::prems = Goalw [Image_def]
-    "[| b: r```A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P";
+    "[| b: r``A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P";
 by (rtac (major RS CollectE) 1);
 by (Clarify_tac 1);
 by (rtac (hd prems) 1);
@@ -364,58 +364,58 @@
 AddSEs [ImageE];
 
 (*This version's more effective when we already have the required "a"*)
-Goal  "[| a:A;  (a,b): r |] ==> b : r```A";
+Goal  "[| a:A;  (a,b): r |] ==> b : r``A";
 by (Blast_tac 1);
 qed "rev_ImageI";
 
-Goal "R```{} = {}";
+Goal "R``{} = {}";
 by (Blast_tac 1);
 qed "Image_empty";
 
 Addsimps [Image_empty];
 
-Goal "Id ``` A = A";
+Goal "Id `` A = A";
 by (Blast_tac 1);
 qed "Image_Id";
 
-Goal "diag A ``` B = A Int B";
+Goal "diag A `` B = A Int B";
 by (Blast_tac 1);
 qed "Image_diag";
 
 Addsimps [Image_Id, Image_diag];
 
-Goal "R ``` (A Int B) <= R ``` A Int R ``` B";
+Goal "R `` (A Int B) <= R `` A Int R `` B";
 by (Blast_tac 1);
 qed "Image_Int_subset";
 
-Goal "R ``` (A Un B) = R ``` A Un R ``` B";
+Goal "R `` (A Un B) = R `` A Un R `` B";
 by (Blast_tac 1);
 qed "Image_Un";
 
-Goal "r <= A <*> B ==> r```C <= B";
+Goal "r <= A <*> B ==> r``C <= B";
 by (rtac subsetI 1);
 by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ;
 qed "Image_subset";
 
 (*NOT suitable for rewriting*)
-Goal "r```B = (UN y: B. r```{y})";
+Goal "r``B = (UN y: B. r``{y})";
 by (Blast_tac 1);
 qed "Image_eq_UN";
 
-Goal "[| r'<=r; A'<=A |] ==> (r' ``` A') <= (r ``` A)";
+Goal "[| r'<=r; A'<=A |] ==> (r' `` A') <= (r `` A)";
 by (Blast_tac 1);
 qed "Image_mono";
 
-Goal "(r ``` (UNION A B)) = (UN x:A.(r ``` (B x)))";
+Goal "(r `` (UNION A B)) = (UN x:A.(r `` (B x)))";
 by (Blast_tac 1);
 qed "Image_UN";
 
 (*Converse inclusion fails*)
-Goal "(r ``` (INTER A B)) <= (INT x:A.(r ``` (B x)))";
+Goal "(r `` (INTER A B)) <= (INT x:A.(r `` (B x)))";
 by (Blast_tac 1);
 qed "Image_INT_subset";
 
-Goal "(r```A <= B) = (A <= - ((r^-1) ``` (-B)))";
+Goal "(r``A <= B) = (A <= - ((r^-1) `` (-B)))";
 by (Blast_tac 1);
 qed "Image_subset_eq";
 
@@ -442,7 +442,7 @@
 by Auto_tac; 
 qed "Range_Collect_split";
 
-Goal "{(x,y). P x y} ``` A = {y. EX x:A. P x y}";
+Goal "{(x,y). P x y} `` A = {y. EX x:A. P x y}";
 by Auto_tac; 
 qed "Image_Collect_split";
 
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Relation.thy	Tue Jan 09 15:22:13 2001 +0100
@@ -16,8 +16,8 @@
   comp  :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set"  (infixr "O" 60)
     "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
 
-  Image :: "[('a*'b) set,'a set] => 'b set"                (infixl "```" 90)
-    "r ``` s == {y. ? x:s. (x,y):r}"
+  Image :: "[('a*'b) set,'a set] => 'b set"                (infixl "``" 90)
+    "r `` s == {y. ? x:s. (x,y):r}"
 
   Id    :: "('a * 'a)set"                            (*the identity relation*)
     "Id == {p. ? x. p = (x,x)}"
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Set.ML	Tue Jan 09 15:22:13 2001 +0100
@@ -531,7 +531,7 @@
 Addsimps [singleton_conv2];
 
 
-section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
+section "Unions of families -- UNION x:A. B(x) is Union(B`A)";
 
 Goalw [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))";
 by (Blast_tac 1);
@@ -561,7 +561,7 @@
 Addcongs [UN_cong];
 
 
-section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
+section "Intersections of families -- INTER x:A. B(x) is Inter(B`A)";
 
 Goalw [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))";
 by Auto_tac;
@@ -652,7 +652,7 @@
 (*** Image of a set under a function ***)
 
 (*Frequently b does not have the syntactic form of f(x).*)
-Goalw [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
+Goalw [image_def] "[| b=f(x);  x:A |] ==> b : f`A";
 by (Blast_tac 1);
 qed "image_eqI";
 Addsimps [image_eqI];
@@ -660,13 +660,13 @@
 bind_thm ("imageI", refl RS image_eqI);
 
 (*This version's more effective when we already have the required x*)
-Goalw [image_def] "[| x:A;  b=f(x) |] ==> b : f``A";
+Goalw [image_def] "[| x:A;  b=f(x) |] ==> b : f`A";
 by (Blast_tac 1);
 qed "rev_image_eqI";
 
 (*The eta-expansion gives variable-name preservation.*)
 val major::prems = Goalw [image_def]
-    "[| b : (%x. f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
+    "[| b : (%x. f(x))`A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
 by (rtac (major RS CollectD RS bexE) 1);
 by (REPEAT (ares_tac prems 1));
 qed "imageE";
@@ -674,22 +674,22 @@
 AddIs  [image_eqI];
 AddSEs [imageE]; 
 
-Goal "f``(A Un B) = f``A Un f``B";
+Goal "f`(A Un B) = f`A Un f`B";
 by (Blast_tac 1);
 qed "image_Un";
 
-Goal "(z : f``A) = (EX x:A. z = f x)";
+Goal "(z : f`A) = (EX x:A. z = f x)";
 by (Blast_tac 1);
 qed "image_iff";
 
 (*This rewrite rule would confuse users if made default.*)
-Goal "(f``A <= B) = (ALL x:A. f(x): B)";
+Goal "(f`A <= B) = (ALL x:A. f(x): B)";
 by (Blast_tac 1);
 qed "image_subset_iff";
 
 (*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
   many existing proofs.*)
-val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
+val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f`A <= B";
 by (blast_tac (claset() addIs prems) 1);
 qed "image_subsetI";
 
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Set.thy	Tue Jan 09 15:22:13 2001 +0100
@@ -34,7 +34,7 @@
   Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
   Pow           :: 'a set => 'a set set                 (*powerset*)
   Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
-  "image"       :: ['a => 'b, 'a set] => ('b set)   (infixr "``" 90)
+  "image"       :: ['a => 'b, 'a set] => ('b set)   (infixr "`" 90)
   (*membership*)
   "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
 
@@ -70,7 +70,7 @@
   "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
 
 translations
-  "range f"     == "f``UNIV"
+  "range f"     == "f`UNIV"
   "x ~: y"      == "~ (x : y)"
   "{x, xs}"     == "insert x {xs}"
   "{x}"         == "insert x {}"
@@ -145,7 +145,7 @@
   empty_def     "{}             == {x. False}"
   UNIV_def      "UNIV           == {x. True}"
   insert_def    "insert a B     == {x. x=a} Un B"
-  image_def     "f``A           == {y. ? x:A. y=f(x)}"
+  image_def     "f`A           == {y. ? x:A. y=f(x)}"
 
 
 end
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Sum_Type.thy	Tue Jan 09 15:22:13 2001 +0100
@@ -40,7 +40,7 @@
   Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
   Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
 
-  sum_def       "A <+> B == (Inl``A) Un (Inr``B)"
+  sum_def       "A <+> B == (Inl`A) Un (Inr`B)"
 
   (*for selecting out the components of a mutually recursive definition*)
   Part_def      "Part A h == A Int {x. ? z. x = h(z)}"
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Wellfounded_Recursion.ML
--- a/src/HOL/Wellfounded_Recursion.ML	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Wellfounded_Recursion.ML	Tue Jan 09 15:22:13 2001 +0100
@@ -193,7 +193,7 @@
  * Wellfoundedness of `image'
  *---------------------------------------------------------------------------*)
 
-Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)";
+Goal "[| wf r; inj f |] ==> wf(prod_fun f f ` r)";
 by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
 by (Clarify_tac 1);
 by (case_tac "EX p. f p : Q" 1);
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/equalities.ML	Tue Jan 09 15:22:13 2001 +0100
@@ -112,49 +112,49 @@
 by (Blast_tac 1);
 qed "UN_insert_distrib";
 
-section "``";
+section "`";
 
-Goal "f``{} = {}";
+Goal "f`{} = {}";
 by (Blast_tac 1);
 qed "image_empty";
 Addsimps[image_empty];
 
-Goal "f``insert a B = insert (f a) (f``B)";
+Goal "f`insert a B = insert (f a) (f`B)";
 by (Blast_tac 1);
 qed "image_insert";
 Addsimps[image_insert];
 
-Goal "x:A ==> (%x. c) `` A = {c}";
+Goal "x:A ==> (%x. c) ` A = {c}";
 by (Blast_tac 1);
 qed "image_constant";
 
-Goal "f``(g``A) = (%x. f (g x)) `` A";
+Goal "f`(g`A) = (%x. f (g x)) ` A";
 by (Blast_tac 1);
 qed "image_image";
 
-Goal "x:A ==> insert (f x) (f``A) = f``A";
+Goal "x:A ==> insert (f x) (f`A) = f`A";
 by (Blast_tac 1);
 qed "insert_image";
 Addsimps [insert_image];
 
-Goal "(f``A = {}) = (A = {})";
+Goal "(f`A = {}) = (A = {})";
 by (blast_tac (claset() addSEs [equalityCE]) 1);
 qed "image_is_empty";
 AddIffs [image_is_empty];
 
-Goal "f `` {x. P x} = {f x | x. P x}";
+Goal "f ` {x. P x} = {f x | x. P x}";
 by (Blast_tac 1);
 qed "image_Collect";
 Addsimps [image_Collect];
 
-Goalw [image_def] "(%x. if P x then f x else g x) `` S   \
-\                = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";
+Goalw [image_def] "(%x. if P x then f x else g x) ` S   \
+\                = (f ` (S Int {x. P x})) Un (g ` (S Int {x. ~(P x)}))";
 by (Simp_tac 1);
 by (Blast_tac 1);
 qed "if_image_distrib";
 Addsimps[if_image_distrib];
 
-val prems = Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
+val prems = Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f`M = g`N";
 by (simp_tac (simpset() addsimps image_def::prems) 1);
 qed "image_cong";
 
@@ -165,7 +165,7 @@
 by Auto_tac;
 qed "full_SetCompr_eq";
 
-Goal "range (%x. f (g x)) = f``range g";
+Goal "range (%x. f (g x)) = f`range g";
 by (stac image_image 1);
 by (Simp_tac 1);
 qed "range_composition";
@@ -563,16 +563,16 @@
 by (Blast_tac 1);
 qed "INT_insert_distrib";
 
-Goal "Union(B``A) = (UN x:A. B(x))";
+Goal "Union(B`A) = (UN x:A. B(x))";
 by (Blast_tac 1);
 qed "Union_image_eq";
 Addsimps [Union_image_eq];
 
-Goal "f `` Union S = (UN x:S. f `` x)";
+Goal "f ` Union S = (UN x:S. f ` x)";
 by (Blast_tac 1);
 qed "image_Union";
 
-Goal "Inter(B``A) = (INT x:A. B(x))";
+Goal "Inter(B`A) = (INT x:A. B(x))";
 by (Blast_tac 1);
 qed "Inter_image_eq";
 Addsimps [Inter_image_eq];
@@ -614,7 +614,7 @@
 
 (* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
    Union of a family of unions **)
-Goal "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
+Goal "(UN x:C. A(x) Un B(x)) = Union(A`C)  Un  Union(B`C)";
 by (Blast_tac 1);
 qed "Un_Union_image";
 
@@ -627,7 +627,7 @@
 by (Blast_tac 1);
 qed "Un_Inter";
 
-Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
+Goal "(INT x:C. A(x) Int B(x)) = Inter(A`C) Int Inter(B`C)";
 by (Blast_tac 1);
 qed "Int_Inter_image";
 
@@ -842,7 +842,7 @@
 qed "Pow_empty";
 Addsimps [Pow_empty];
 
-Goal "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
+Goal "Pow (insert a A) = Pow A Un (insert a ` Pow A)";
 by (blast_tac (claset() addIs [inst "x" "?u-{a}" image_eqI]) 1);
 qed "Pow_insert";
 
@@ -922,7 +922,7 @@
      "(UN x:C. A - B x)    = (A - (INT x:C. B x))",
      "(UN x: Union A. B x) = (UN y:A. UN x:y. B x)",
      "(UN z: UNION A B. C z) = (UN  x:A. UN z: B(x). C z)",
-     "(UN x:f``A. B x)     = (UN a:A. B(f a))"];
+     "(UN x:f`A. B x)     = (UN a:A. B(f a))"];
 
 val INT_simps = map prover
     ["!!C. c: C ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
@@ -934,7 +934,7 @@
      "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))",
      "(INT x: Union A. B x) = (INT y:A. INT x:y. B x)",
      "(INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)",
-     "(INT x:f``A. B x)    = (INT a:A. B(f a))"];
+     "(INT x:f`A. B x)    = (INT a:A. B(f a))"];
 
 
 val ball_simps = map prover
@@ -948,7 +948,7 @@
      "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
      "(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)",
      "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",
-     "(ALL x:f``A. P x) = (ALL x:A. P(f x))",
+     "(ALL x:f`A. P x) = (ALL x:A. P(f x))",
      "(~(ALL x:A. P x)) = (EX x:A. ~P x)"];
 
 val ball_conj_distrib = 
@@ -963,7 +963,7 @@
      "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
      "(EX x: UNION A B. P x) = (EX a:A. EX x: B a.  P x)",
      "(EX x:Collect Q. P x) = (EX x. Q x & P x)",
-     "(EX x:f``A. P x) = (EX x:A. P(f x))",
+     "(EX x:f`A. P x) = (EX x:A. P(f x))",
      "(~(EX x:A. P x)) = (ALL x:A. ~P x)"];
 
 val bex_disj_distrib = 
diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/mono.ML
--- a/src/HOL/mono.ML	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/mono.ML	Tue Jan 09 15:22:13 2001 +0100
@@ -6,7 +6,7 @@
 Monotonicity of various operations
 *)
 
-Goal "A<=B ==> f``A <= f``B";
+Goal "A<=B ==> f`A <= f`B";
 by (Blast_tac 1);
 qed "image_mono";
 
@@ -107,7 +107,7 @@
 (* Courtesy of Stephan Merz *)
 Goalw [Least_def,mono_def]
   "[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \
-\  ==> (LEAST y. y : f``S) = f(LEAST x. x : S)";
+\  ==> (LEAST y. y : f`S) = f(LEAST x. x : S)";
 by (etac bexE 1);
 by (rtac someI2 1);
 by (Force_tac 1);