*** empty log message ***
authornipkow
Tue, 09 Jan 2001 15:32:27 +0100
changeset 10834 a7897aebbffc
parent 10833 c0844a30ea4e
child 10835 f4745d77e620
*** empty log message ***
src/HOL/Hyperreal/HRealAbs.ML
src/HOL/Hyperreal/HSeries.ML
src/HOL/Hyperreal/HSeries.thy
src/HOL/Hyperreal/HyperDef.ML
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperNat.ML
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Hyperreal/HyperPow.ML
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Hyperreal/Lim.ML
src/HOL/Hyperreal/NSA.ML
src/HOL/Hyperreal/NatStar.ML
src/HOL/Hyperreal/NatStar.thy
src/HOL/Hyperreal/SEQ.ML
src/HOL/Hyperreal/Star.ML
src/HOL/Hyperreal/Star.thy
src/HOL/IMPP/Hoare.ML
src/HOL/IMPP/Hoare.thy
src/HOL/Induct/LList.ML
src/HOL/Induct/LList.thy
src/HOL/Integ/Equiv.ML
src/HOL/Integ/Equiv.thy
src/HOL/Integ/IntDef.ML
src/HOL/Integ/IntDef.thy
src/HOL/Integ/int_arith1.ML
src/HOL/Lattice/Bounds.thy
src/HOL/Lattice/CompleteLattice.thy
src/HOL/Lattice/Orders.thy
src/HOL/Lex/Automata.ML
src/HOL/Lex/Automata.thy
src/HOL/Lex/NA.thy
src/HOL/Lex/NAe.ML
src/HOL/Lex/NAe.thy
src/HOL/Lex/RegExp2NA.thy
src/HOL/Lex/RegExp2NAe.thy
src/HOL/MicroJava/BV/JVM.thy
src/HOL/MicroJava/J/JBasis.ML
src/HOL/NumberTheory/BijectionRel.ML
src/HOL/NumberTheory/EulerFermat.ML
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/NumberTheory/WilsonBij.ML
src/HOL/Real/PNat.ML
src/HOL/Real/PNat.thy
src/HOL/Real/PRat.ML
src/HOL/Real/PRat.thy
src/HOL/Real/PReal.ML
src/HOL/Real/RealDef.ML
src/HOL/Real/RealDef.thy
src/HOL/Real/RealInt.ML
src/HOL/Real/RealInt.thy
src/HOL/UNITY/Channel.ML
src/HOL/UNITY/Channel.thy
src/HOL/UNITY/ELT.ML
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/FP.ML
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/PPROD.ML
src/HOL/UNITY/PriorityAux.ML
src/HOL/UNITY/PriorityAux.thy
src/HOL/UNITY/Project.ML
src/HOL/UNITY/Reach.ML
src/HOL/UNITY/Rename.ML
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/Token.ML
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/WFair.ML
src/HOL/UNITY/WFair.thy
src/HOL/ex/Multiquote.thy
src/HOL/ex/PiSets.ML
src/HOL/ex/Tarski.ML
src/HOL/ex/Tarski.thy
src/HOL/ex/set.ML
src/HOLCF/Cfun1.ML
src/HOLCF/Cfun1.thy
src/HOLCF/Cfun2.ML
src/HOLCF/Cfun3.ML
src/HOLCF/Cfun3.thy
src/HOLCF/Cprod3.ML
src/HOLCF/Cprod3.thy
src/HOLCF/Fix.ML
src/HOLCF/Fix.thy
src/HOLCF/Lift.ML
src/HOLCF/Lift3.ML
src/HOLCF/Lift3.thy
src/HOLCF/Sprod3.ML
src/HOLCF/Sprod3.thy
src/HOLCF/Ssum0.ML
src/HOLCF/Ssum0.thy
src/HOLCF/Ssum3.ML
src/HOLCF/Ssum3.thy
src/HOLCF/Tr.ML
src/HOLCF/Tr.thy
src/HOLCF/Up1.ML
src/HOLCF/Up1.thy
src/HOLCF/Up3.ML
src/HOLCF/Up3.thy
--- a/src/HOL/Hyperreal/HRealAbs.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HRealAbs.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -19,8 +19,8 @@
 Addsimps [hrabs_number_of];
 
 Goalw [hrabs_def]
-     "abs (Abs_hypreal (hyprel ``` {X})) = \
-\     Abs_hypreal(hyprel ``` {%n. abs (X n)})";
+     "abs (Abs_hypreal (hyprel `` {X})) = \
+\     Abs_hypreal(hyprel `` {%n. abs (X n)})";
 by (auto_tac (claset(),
               simpset_of HyperDef.thy 
                   addsimps [hypreal_zero_def, hypreal_le,hypreal_minus]));
@@ -232,7 +232,7 @@
 (*------------------------------------------------------------*)
 
 Goalw [hypreal_of_nat_def, hypreal_of_real_def, real_of_nat_def] 
-     "hypreal_of_nat  m = Abs_hypreal(hyprel```{%n. real_of_nat m})";
+     "hypreal_of_nat  m = Abs_hypreal(hyprel``{%n. real_of_nat m})";
 by Auto_tac;
 qed "hypreal_of_nat_iff";
 
--- a/src/HOL/Hyperreal/HSeries.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HSeries.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -8,14 +8,14 @@
 Goalw [sumhr_def]
      "sumhr(M,N,f) =  \
 \       Abs_hypreal(UN X:Rep_hypnat(M). UN Y: Rep_hypnat(N). \
-\         hyprel ```{%n::nat. sumr (X n) (Y n) f})";
+\         hyprel ``{%n::nat. sumr (X n) (Y n) f})";
 by (Auto_tac);
 qed "sumhr_iff";
 
 Goalw [sumhr_def]
-     "sumhr(Abs_hypnat(hypnatrel```{%n. M n}), \
-\           Abs_hypnat(hypnatrel```{%n. N n}), f) = \
-\     Abs_hypreal(hyprel ``` {%n. sumr (M n) (N n) f})";
+     "sumhr(Abs_hypnat(hypnatrel``{%n. M n}), \
+\           Abs_hypnat(hypnatrel``{%n. N n}), f) = \
+\     Abs_hypreal(hyprel `` {%n. sumr (M n) (N n) f})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
 by (Auto_tac THEN Ultra_tac 1);
 qed "sumhr";
@@ -27,7 +27,7 @@
 Goalw [sumhr_def]
       "sumhr p = (%(M,N,f). Abs_hypreal(UN X:Rep_hypnat(M). \
 \                     UN Y: Rep_hypnat(N). \
-\           hyprel ```{%n::nat. sumr (X n) (Y n) f})) p";
+\           hyprel ``{%n::nat. sumr (X n) (Y n) f})) p";
 by (res_inst_tac [("p","p")] PairE 1);
 by (res_inst_tac [("p","y")] PairE 1);
 by (Auto_tac);
--- a/src/HOL/Hyperreal/HSeries.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -15,7 +15,7 @@
    "sumhr p
        == Abs_hypreal(UN X:Rep_hypnat(fst p). 
               UN Y: Rep_hypnat(fst(snd p)).
-              hyprel```{%n::nat. sumr (X n) (Y n) (snd(snd p))})"
+              hyprel``{%n::nat. sumr (X n) (Y n) (snd(snd p))})"
 
 constdefs
    NSsums  :: [nat=>real,real] => bool     (infixr 80)
--- a/src/HOL/Hyperreal/HyperDef.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HyperDef.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -206,11 +206,11 @@
 	      simpset() addsimps [FreeUltrafilterNat_Nat_set]));
 qed "equiv_hyprel";
 
-(* (hyprel ``` {x} = hyprel ``` {y}) = ((x,y) : hyprel) *)
+(* (hyprel `` {x} = hyprel `` {y}) = ((x,y) : hyprel) *)
 bind_thm ("equiv_hyprel_iff",
     	  [equiv_hyprel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
 
-Goalw  [hypreal_def,hyprel_def,quotient_def] "hyprel```{x}:hypreal";
+Goalw  [hypreal_def,hyprel_def,quotient_def] "hyprel``{x}:hypreal";
 by (Blast_tac 1);
 qed "hyprel_in_hypreal";
 
@@ -230,7 +230,7 @@
 by (rtac Rep_hypreal_inverse 1);
 qed "inj_Rep_hypreal";
 
-Goalw [hyprel_def] "x: hyprel ``` {x}";
+Goalw [hyprel_def] "x: hyprel `` {x}";
 by (Step_tac 1);
 by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset()));
 qed "lemma_hyprel_refl";
@@ -267,7 +267,7 @@
 qed "inj_hypreal_of_real";
 
 val [prem] = goal (the_context ())
-    "(!!x y. z = Abs_hypreal(hyprel```{x}) ==> P) ==> P";
+    "(!!x y. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P";
 by (res_inst_tac [("x1","z")] 
     (rewrite_rule [hypreal_def] Rep_hypreal RS quotientE) 1);
 by (dres_inst_tac [("f","Abs_hypreal")] arg_cong 1);
@@ -278,13 +278,13 @@
 (**** hypreal_minus: additive inverse on hypreal ****)
 
 Goalw [congruent_def]
-  "congruent hyprel (%X. hyprel```{%n. - (X n)})";
+  "congruent hyprel (%X. hyprel``{%n. - (X n)})";
 by Safe_tac;
 by (ALLGOALS Ultra_tac);
 qed "hypreal_minus_congruent";
 
 Goalw [hypreal_minus_def]
-   "- (Abs_hypreal(hyprel```{%n. X n})) = Abs_hypreal(hyprel ``` {%n. -(X n)})";
+   "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
 by (simp_tac (simpset() addsimps 
       [hyprel_in_hypreal RS Abs_hypreal_inverse,
@@ -322,20 +322,20 @@
 (**** hyperreal addition: hypreal_add  ****)
 
 Goalw [congruent2_def]
-    "congruent2 hyprel (%X Y. hyprel```{%n. X n + Y n})";
+    "congruent2 hyprel (%X Y. hyprel``{%n. X n + Y n})";
 by Safe_tac;
 by (ALLGOALS(Ultra_tac));
 qed "hypreal_add_congruent2";
 
 Goalw [hypreal_add_def]
-  "Abs_hypreal(hyprel```{%n. X n}) + Abs_hypreal(hyprel```{%n. Y n}) = \
-\  Abs_hypreal(hyprel```{%n. X n + Y n})";
+  "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) = \
+\  Abs_hypreal(hyprel``{%n. X n + Y n})";
 by (simp_tac (simpset() addsimps 
          [[equiv_hyprel, hypreal_add_congruent2] MRS UN_equiv_class2]) 1);
 qed "hypreal_add";
 
-Goal "Abs_hypreal(hyprel```{%n. X n}) - Abs_hypreal(hyprel```{%n. Y n}) = \
-\     Abs_hypreal(hyprel```{%n. X n - Y n})";
+Goal "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) = \
+\     Abs_hypreal(hyprel``{%n. X n - Y n})";
 by (simp_tac (simpset() addsimps 
          [hypreal_diff_def, hypreal_minus,hypreal_add]) 1);
 qed "hypreal_diff";
@@ -496,14 +496,14 @@
 (**** hyperreal multiplication: hypreal_mult  ****)
 
 Goalw [congruent2_def]
-    "congruent2 hyprel (%X Y. hyprel```{%n. X n * Y n})";
+    "congruent2 hyprel (%X Y. hyprel``{%n. X n * Y n})";
 by Safe_tac;
 by (ALLGOALS(Ultra_tac));
 qed "hypreal_mult_congruent2";
 
 Goalw [hypreal_mult_def]
-  "Abs_hypreal(hyprel```{%n. X n}) * Abs_hypreal(hyprel```{%n. Y n}) = \
-\  Abs_hypreal(hyprel```{%n. X n * Y n})";
+  "Abs_hypreal(hyprel``{%n. X n}) * Abs_hypreal(hyprel``{%n. Y n}) = \
+\  Abs_hypreal(hyprel``{%n. X n * Y n})";
 by (simp_tac (simpset() addsimps 
       [[equiv_hyprel, hypreal_mult_congruent2] MRS UN_equiv_class2]) 1);
 qed "hypreal_mult";
@@ -622,13 +622,13 @@
 (**** multiplicative inverse on hypreal ****)
 
 Goalw [congruent_def]
-  "congruent hyprel (%X. hyprel```{%n. if X n = #0 then #0 else inverse(X n)})";
+  "congruent hyprel (%X. hyprel``{%n. if X n = #0 then #0 else inverse(X n)})";
 by (Auto_tac THEN Ultra_tac 1);
 qed "hypreal_inverse_congruent";
 
 Goalw [hypreal_inverse_def]
-      "inverse (Abs_hypreal(hyprel```{%n. X n})) = \
-\      Abs_hypreal(hyprel ``` {%n. if X n = #0 then #0 else inverse(X n)})";
+      "inverse (Abs_hypreal(hyprel``{%n. X n})) = \
+\      Abs_hypreal(hyprel `` {%n. if X n = #0 then #0 else inverse(X n)})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
 by (simp_tac (simpset() addsimps 
    [hyprel_in_hypreal RS Abs_hypreal_inverse,
@@ -800,8 +800,8 @@
   makes many of them more straightforward. 
  -------------------------------------------------------*)
 Goalw [hypreal_less_def]
-      "(Abs_hypreal(hyprel```{%n. X n}) < \
-\           Abs_hypreal(hyprel```{%n. Y n})) = \
+      "(Abs_hypreal(hyprel``{%n. X n}) < \
+\           Abs_hypreal(hyprel``{%n. Y n})) = \
 \      ({n. X n < Y n} : FreeUltrafilterNat)";
 by (auto_tac (claset() addSIs [lemma_hyprel_refl], simpset()));
 by (Ultra_tac 1);
@@ -840,7 +840,7 @@
                          Trichotomy of the hyperreals
   --------------------------------------------------------------------------------*)
 
-Goalw [hyprel_def] "EX x. x: hyprel ``` {%n. #0}";
+Goalw [hyprel_def] "EX x. x: hyprel `` {%n. #0}";
 by (res_inst_tac [("x","%n. #0")] exI 1);
 by (Step_tac 1);
 by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset()));
@@ -958,8 +958,8 @@
 (*------ hypreal le iff reals le a.e ------*)
 
 Goalw [hypreal_le_def,real_le_def]
-      "(Abs_hypreal(hyprel```{%n. X n}) <= \
-\           Abs_hypreal(hyprel```{%n. Y n})) = \
+      "(Abs_hypreal(hyprel``{%n. X n}) <= \
+\           Abs_hypreal(hyprel``{%n. Y n})) = \
 \      ({n. X n <= Y n} : FreeUltrafilterNat)";
 by (auto_tac (claset(),simpset() addsimps [hypreal_less]));
 by (ALLGOALS(Ultra_tac));
--- a/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -37,28 +37,28 @@
 defs
 
   hypreal_zero_def
-  "0 == Abs_hypreal(hyprel```{%n::nat. (#0::real)})"
+  "0 == Abs_hypreal(hyprel``{%n::nat. (#0::real)})"
 
   hypreal_one_def
-  "1hr == Abs_hypreal(hyprel```{%n::nat. (#1::real)})"
+  "1hr == Abs_hypreal(hyprel``{%n::nat. (#1::real)})"
 
   (* an infinite number = [<1,2,3,...>] *)
   omega_def
-  "whr == Abs_hypreal(hyprel```{%n::nat. real_of_nat (Suc n)})"
+  "whr == Abs_hypreal(hyprel``{%n::nat. real_of_nat (Suc n)})"
     
   (* an infinitesimal number = [<1,1/2,1/3,...>] *)
   epsilon_def
-  "ehr == Abs_hypreal(hyprel```{%n::nat. inverse (real_of_nat (Suc n))})"
+  "ehr == Abs_hypreal(hyprel``{%n::nat. inverse (real_of_nat (Suc n))})"
 
   hypreal_minus_def
-  "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel```{%n::nat. - (X n)})"
+  "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
 
   hypreal_diff_def 
   "x - y == x + -(y::hypreal)"
 
   hypreal_inverse_def
   "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). 
-                    hyprel```{%n. if X n = #0 then #0 else inverse (X n)})"
+                    hyprel``{%n. if X n = #0 then #0 else inverse (X n)})"
 
   hypreal_divide_def
   "P / Q::hypreal == P * inverse Q"
@@ -66,17 +66,17 @@
 constdefs
 
   hypreal_of_real  :: real => hypreal                 
-  "hypreal_of_real r         == Abs_hypreal(hyprel```{%n::nat. r})"
+  "hypreal_of_real r         == Abs_hypreal(hyprel``{%n::nat. r})"
 
 defs 
 
   hypreal_add_def  
   "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
-                hyprel```{%n::nat. X n + Y n})"
+                hyprel``{%n::nat. X n + Y n})"
 
   hypreal_mult_def  
   "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
-                hyprel```{%n::nat. X n * Y n})"
+                hyprel``{%n::nat. X n * Y n})"
 
   hypreal_less_def
   "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & 
--- a/src/HOL/Hyperreal/HyperNat.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HyperNat.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -65,7 +65,7 @@
 val equiv_hypnatrel_iff =
     [UNIV_I, UNIV_I] MRS (equiv_hypnatrel RS eq_equiv_class_iff);
 
-Goalw  [hypnat_def,hypnatrel_def,quotient_def] "hypnatrel```{x}:hypnat";
+Goalw  [hypnat_def,hypnatrel_def,quotient_def] "hypnatrel``{x}:hypnat";
 by (Blast_tac 1);
 qed "hypnatrel_in_hypnat";
 
@@ -85,7 +85,7 @@
 by (rtac Rep_hypnat_inverse 1);
 qed "inj_Rep_hypnat";
 
-Goalw [hypnatrel_def] "x: hypnatrel ``` {x}";
+Goalw [hypnatrel_def] "x: hypnatrel `` {x}";
 by (Step_tac 1);
 by Auto_tac;
 qed "lemma_hypnatrel_refl";
@@ -121,7 +121,7 @@
 qed "inj_hypnat_of_nat";
 
 val [prem] = Goal
-    "(!!x. z = Abs_hypnat(hypnatrel```{x}) ==> P) ==> P";
+    "(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P";
 by (res_inst_tac [("x1","z")] 
     (rewrite_rule [hypnat_def] Rep_hypnat RS quotientE) 1);
 by (dres_inst_tac [("f","Abs_hypnat")] arg_cong 1);
@@ -133,14 +133,14 @@
    Addition for hyper naturals: hypnat_add 
  -----------------------------------------------------------*)
 Goalw [congruent2_def]
-     "congruent2 hypnatrel (%X Y. hypnatrel```{%n. X n + Y n})";
+     "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})";
 by Safe_tac;
 by (ALLGOALS(Fuf_tac));
 qed "hypnat_add_congruent2";
 
 Goalw [hypnat_add_def]
-  "Abs_hypnat(hypnatrel```{%n. X n}) + Abs_hypnat(hypnatrel```{%n. Y n}) = \
-\  Abs_hypnat(hypnatrel```{%n. X n + Y n})";
+  "Abs_hypnat(hypnatrel``{%n. X n}) + Abs_hypnat(hypnatrel``{%n. Y n}) = \
+\  Abs_hypnat(hypnatrel``{%n. X n + Y n})";
 by (asm_simp_tac
     (simpset() addsimps [[equiv_hypnatrel, hypnat_add_congruent2] 
      MRS UN_equiv_class2]) 1);
@@ -186,14 +186,14 @@
    Subtraction for hyper naturals: hypnat_minus
  -----------------------------------------------------------*)
 Goalw [congruent2_def]
-    "congruent2 hypnatrel (%X Y. hypnatrel```{%n. X n - Y n})";
+    "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})";
 by Safe_tac;
 by (ALLGOALS(Fuf_tac));
 qed "hypnat_minus_congruent2";
  
 Goalw [hypnat_minus_def]
-  "Abs_hypnat(hypnatrel```{%n. X n}) - Abs_hypnat(hypnatrel```{%n. Y n}) = \
-\  Abs_hypnat(hypnatrel```{%n. X n - Y n})";
+  "Abs_hypnat(hypnatrel``{%n. X n}) - Abs_hypnat(hypnatrel``{%n. Y n}) = \
+\  Abs_hypnat(hypnatrel``{%n. X n - Y n})";
 by (asm_simp_tac
     (simpset() addsimps [[equiv_hypnatrel, hypnat_minus_congruent2] 
      MRS UN_equiv_class2]) 1);
@@ -273,14 +273,14 @@
    Multiplication for hyper naturals: hypnat_mult
  -----------------------------------------------------------*)
 Goalw [congruent2_def]
-    "congruent2 hypnatrel (%X Y. hypnatrel```{%n. X n * Y n})";
+    "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})";
 by Safe_tac;
 by (ALLGOALS(Fuf_tac));
 qed "hypnat_mult_congruent2";
 
 Goalw [hypnat_mult_def]
-  "Abs_hypnat(hypnatrel```{%n. X n}) * Abs_hypnat(hypnatrel```{%n. Y n}) = \
-\  Abs_hypnat(hypnatrel```{%n. X n * Y n})";
+  "Abs_hypnat(hypnatrel``{%n. X n}) * Abs_hypnat(hypnatrel``{%n. Y n}) = \
+\  Abs_hypnat(hypnatrel``{%n. X n * Y n})";
 by (asm_simp_tac
     (simpset() addsimps [[equiv_hypnatrel,hypnat_mult_congruent2] MRS
      UN_equiv_class2]) 1);
@@ -475,8 +475,8 @@
 (* See comments in HYPER for corresponding thm *)
 
 Goalw [hypnat_less_def]
-      "(Abs_hypnat(hypnatrel```{%n. X n}) < \
-\           Abs_hypnat(hypnatrel```{%n. Y n})) = \
+      "(Abs_hypnat(hypnatrel``{%n. X n}) < \
+\           Abs_hypnat(hypnatrel``{%n. Y n})) = \
 \      ({n. X n < Y n} : FreeUltrafilterNat)";
 by (auto_tac (claset() addSIs [lemma_hypnatrel_refl],simpset()));
 by (Fuf_tac 1);
@@ -527,7 +527,7 @@
 (*---------------------------------------------------------------------------------
                    Trichotomy of the hyper naturals
   --------------------------------------------------------------------------------*)
-Goalw [hypnatrel_def] "EX x. x: hypnatrel ``` {%n. 0}";
+Goalw [hypnatrel_def] "EX x. x: hypnatrel `` {%n. 0}";
 by (res_inst_tac [("x","%n. 0")] exI 1);
 by (Step_tac 1);
 by Auto_tac;
@@ -620,8 +620,8 @@
 
 (*------ hypnat le iff nat le a.e ------*)
 Goalw [hypnat_le_def,le_def]
-      "(Abs_hypnat(hypnatrel```{%n. X n}) <= \
-\           Abs_hypnat(hypnatrel```{%n. Y n})) = \
+      "(Abs_hypnat(hypnatrel``{%n. X n}) <= \
+\           Abs_hypnat(hypnatrel``{%n. Y n})) = \
 \      ({n. X n <= Y n} : FreeUltrafilterNat)";
 by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
     simpset() addsimps [hypnat_less]));
@@ -833,7 +833,7 @@
               Existence of infinite hypernatural number
  ---------------------------------------------------------------------------------*)
 
-Goal "hypnatrel```{%n::nat. n} : hypnat";
+Goal "hypnatrel``{%n::nat. n} : hypnat";
 by Auto_tac;
 qed "hypnat_omega";
 
@@ -936,23 +936,23 @@
 by Auto_tac;
 qed "SHNat_iff";
 
-Goalw [SHNat_def] "hypnat_of_nat ``(UNIV::nat set) = SNat";
+Goalw [SHNat_def] "hypnat_of_nat `(UNIV::nat set) = SNat";
 by Auto_tac;
 qed "hypnat_of_nat_image";
 
-Goalw [SHNat_def] "inv hypnat_of_nat ``SNat = (UNIV::nat set)";
+Goalw [SHNat_def] "inv hypnat_of_nat `SNat = (UNIV::nat set)";
 by Auto_tac;
 by (rtac (inj_hypnat_of_nat RS inv_f_f RS subst) 1);
 by (Blast_tac 1);
 qed "inv_hypnat_of_nat_image";
 
 Goalw [SHNat_def] 
-     "[| EX x. x: P; P <= SNat |] ==> EX Q. P = hypnat_of_nat `` Q";
+     "[| EX x. x: P; P <= SNat |] ==> EX Q. P = hypnat_of_nat ` Q";
 by (Best_tac 1); 
 qed "SHNat_hypnat_of_nat_image";
 
 Goalw [SHNat_def] 
-      "SNat = hypnat_of_nat `` (UNIV::nat set)";
+      "SNat = hypnat_of_nat ` (UNIV::nat set)";
 by Auto_tac;
 qed "SHNat_hypnat_of_nat_iff";
 
@@ -1066,7 +1066,7 @@
      "HNatInfinite = {N. ALL n:SNat. n < N}";
 by (Step_tac 1);
 by (dres_inst_tac [("x","Abs_hypnat \
-\        (hypnatrel ``` {%n. N})")] bspec 2);
+\        (hypnatrel `` {%n. N})")] bspec 2);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 by (auto_tac (claset(),simpset() addsimps [hypnat_less_iff]));
@@ -1215,14 +1215,14 @@
     Embedding of the hypernaturals into the hyperreal
  --------------------------------------------------------------*)
 
-Goal "(Ya : hyprel ```{%n. f(n)}) = \
+Goal "(Ya : hyprel ``{%n. f(n)}) = \
 \     ({n. f n = Ya n} : FreeUltrafilterNat)";
 by Auto_tac;
 qed "lemma_hyprel_FUFN";
 
 Goalw [hypreal_of_hypnat_def]
-      "hypreal_of_hypnat (Abs_hypnat(hypnatrel```{%n. X n})) = \
-\         Abs_hypreal(hyprel ``` {%n. real_of_nat (X n)})";
+      "hypreal_of_hypnat (Abs_hypnat(hypnatrel``{%n. X n})) = \
+\         Abs_hypreal(hyprel `` {%n. real_of_nat (X n)})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
 by (auto_tac (claset()
                   addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset],
--- a/src/HOL/Hyperreal/HyperNat.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -25,7 +25,7 @@
 
   (* embedding the naturals in the hypernaturals *)
   hypnat_of_nat   :: nat => hypnat
-  "hypnat_of_nat m  == Abs_hypnat(hypnatrel```{%n::nat. m})"
+  "hypnat_of_nat m  == Abs_hypnat(hypnatrel``{%n::nat. m})"
 
   (* hypernaturals as members of the hyperreals; the set is defined as  *)
   (* the nonstandard extension of set of naturals embedded in the reals *)
@@ -39,7 +39,7 @@
   (* explicit embedding of the hypernaturals in the hyperreals *)    
   hypreal_of_hypnat :: hypnat => hypreal
   "hypreal_of_hypnat N  == Abs_hypreal(UN X: Rep_hypnat(N). 
-                            hyprel```{%n::nat. real_of_nat (X n)})"
+                            hyprel``{%n::nat. real_of_nat (X n)})"
   
 defs
 
@@ -53,23 +53,23 @@
 
   (** hypernatural arithmetic **)
   
-  hypnat_zero_def      "0 == Abs_hypnat(hypnatrel```{%n::nat. 0})"
-  hypnat_one_def       "1hn == Abs_hypnat(hypnatrel```{%n::nat. 1})"
+  hypnat_zero_def      "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})"
+  hypnat_one_def       "1hn == Abs_hypnat(hypnatrel``{%n::nat. 1})"
 
   (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
-  hypnat_omega_def     "whn == Abs_hypnat(hypnatrel```{%n::nat. n})"
+  hypnat_omega_def     "whn == Abs_hypnat(hypnatrel``{%n::nat. n})"
  
   hypnat_add_def  
   "P + Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
-                hypnatrel```{%n::nat. X n + Y n})"
+                hypnatrel``{%n::nat. X n + Y n})"
 
   hypnat_mult_def  
   "P * Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
-                hypnatrel```{%n::nat. X n * Y n})"
+                hypnatrel``{%n::nat. X n * Y n})"
 
   hypnat_minus_def  
   "P - Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
-                hypnatrel```{%n::nat. X n - Y n})"
+                hypnatrel``{%n::nat. X n - Y n})"
 
   hypnat_less_def
   "P < (Q::hypnat) == EX X Y. X: Rep_hypnat(P) & 
--- a/src/HOL/Hyperreal/HyperPow.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HyperPow.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -178,7 +178,7 @@
               simpset() addsimps [hypreal_mult_less_mono2]));
 qed_spec_mp "hrealpow_Suc_le";
 
-Goal "Abs_hypreal(hyprel```{%n. X n}) ^ m = Abs_hypreal(hyprel```{%n. (X n) ^ m})";
+Goal "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})";
 by (induct_tac "m" 1);
 by (auto_tac (claset(),
               simpset() delsimps [one_eq_numeral_1]
@@ -221,14 +221,14 @@
  --------------------------------------------------------------*)
 Goalw [congruent_def]
      "congruent hyprel \
-\    (%X Y. hyprel```{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})";
+\    (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})";
 by (safe_tac (claset() addSIs [ext]));
 by (ALLGOALS(Fuf_tac));
 qed "hyperpow_congruent";
 
 Goalw [hyperpow_def]
-  "Abs_hypreal(hyprel```{%n. X n}) pow Abs_hypnat(hypnatrel```{%n. Y n}) = \
-\  Abs_hypreal(hyprel```{%n. X n ^ Y n})";
+  "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) = \
+\  Abs_hypreal(hyprel``{%n. X n ^ Y n})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
 by (auto_tac (claset() addSIs [lemma_hyprel_refl,bexI],
     simpset() addsimps [hyprel_in_hypreal RS 
--- a/src/HOL/Hyperreal/HyperPow.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -32,5 +32,5 @@
   hyperpow_def
   "(R::hypreal) pow (N::hypnat) 
       == Abs_hypreal(UN X:Rep_hypreal(R). UN Y: Rep_hypnat(N).
-             hyprel```{%n::nat. (X n) ^ (Y n)})"
+             hyprel``{%n::nat. (X n) ^ (Y n)})"
 end
--- a/src/HOL/Hyperreal/Lim.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/Lim.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -220,7 +220,7 @@
 by (fold_tac [real_le_def]);
 by (dtac lemma_skolemize_LIM2 1);
 by (Step_tac 1);
-by (dres_inst_tac [("x","Abs_hypreal(hyprel```{X})")] spec 1);
+by (dres_inst_tac [("x","Abs_hypreal(hyprel``{X})")] spec 1);
 by (asm_full_simp_tac
     (simpset() addsimps [starfun, hypreal_minus, 
                          hypreal_of_real_def,hypreal_add]) 1);
@@ -726,8 +726,8 @@
 by (fold_tac [real_le_def]);
 by (dtac lemma_skolemize_LIM2u 1);
 by (Step_tac 1);
-by (dres_inst_tac [("x","Abs_hypreal(hyprel```{X})")] spec 1);
-by (dres_inst_tac [("x","Abs_hypreal(hyprel```{Y})")] spec 1);
+by (dres_inst_tac [("x","Abs_hypreal(hyprel``{X})")] spec 1);
+by (dres_inst_tac [("x","Abs_hypreal(hyprel``{Y})")] spec 1);
 by (asm_full_simp_tac
     (simpset() addsimps [starfun, hypreal_minus,hypreal_add]) 1);
 by Auto_tac;
--- a/src/HOL/Hyperreal/NSA.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/NSA.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -94,18 +94,18 @@
 by Auto_tac;
 qed "SReal_iff";
 
-Goalw [SReal_def] "hypreal_of_real ``(UNIV::real set) = SReal";
+Goalw [SReal_def] "hypreal_of_real `(UNIV::real set) = SReal";
 by Auto_tac;
 qed "hypreal_of_real_image";
 
-Goalw [SReal_def] "inv hypreal_of_real ``SReal = (UNIV::real set)";
+Goalw [SReal_def] "inv hypreal_of_real `SReal = (UNIV::real set)";
 by Auto_tac;
 by (rtac (inj_hypreal_of_real RS inv_f_f RS subst) 1);
 by (Blast_tac 1);
 qed "inv_hypreal_of_real_image";
 
 Goalw [SReal_def] 
-      "[| EX x. x: P; P <= SReal |] ==> EX Q. P = hypreal_of_real `` Q";
+      "[| EX x. x: P; P <= SReal |] ==> EX Q. P = hypreal_of_real ` Q";
 by (Best_tac 1); 
 qed "SReal_hypreal_of_real_image";
 
@@ -140,13 +140,13 @@
     lifting of ub and property of lub
  -------------------------------------------------------*)
 Goalw [isUb_def,setle_def] 
-      "(isUb (SReal) (hypreal_of_real `` Q) (hypreal_of_real Y)) = \
+      "(isUb (SReal) (hypreal_of_real ` Q) (hypreal_of_real Y)) = \
 \      (isUb (UNIV :: real set) Q Y)";
 by Auto_tac;
 qed "hypreal_of_real_isUb_iff";
 
 Goalw [isLub_def,leastP_def] 
-     "isLub SReal (hypreal_of_real `` Q) (hypreal_of_real Y) \
+     "isLub SReal (hypreal_of_real ` Q) (hypreal_of_real Y) \
 \     ==> isLub (UNIV :: real set) Q Y";
 by (auto_tac (claset() addIs [hypreal_of_real_isUb_iff RS iffD2],
               simpset() addsimps [hypreal_of_real_isUb_iff, setge_def]));
@@ -154,7 +154,7 @@
 
 Goalw [isLub_def,leastP_def] 
       "isLub (UNIV :: real set) Q Y \
-\      ==> isLub SReal (hypreal_of_real `` Q) (hypreal_of_real Y)";
+\      ==> isLub SReal (hypreal_of_real ` Q) (hypreal_of_real Y)";
 by (auto_tac (claset(),
               simpset() addsimps [hypreal_of_real_isUb_iff, setge_def]));
 by (forw_inst_tac [("x2","x")] (isUbD2a RS (SReal_iff RS iffD1) RS exE) 1);
@@ -163,7 +163,7 @@
 by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_isUb_iff]));
 qed "hypreal_of_real_isLub2";
 
-Goal "(isLub SReal (hypreal_of_real `` Q) (hypreal_of_real Y)) = \
+Goal "(isLub SReal (hypreal_of_real ` Q) (hypreal_of_real Y)) = \
 \     (isLub (UNIV :: real set) Q Y)";
 by (blast_tac (claset() addIs [hypreal_of_real_isLub1,
                                hypreal_of_real_isLub2]) 1);
@@ -2059,7 +2059,7 @@
        Omega is a member of HInfinite
  -----------------------------------------------*)
 
-Goal "hyprel```{%n::nat. real_of_nat (Suc n)} : hypreal";
+Goal "hyprel``{%n::nat. real_of_nat (Suc n)} : hypreal";
 by Auto_tac;
 qed "hypreal_omega";
 
@@ -2192,7 +2192,7 @@
     |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x|: Infinitesimal 
  -----------------------------------------------------*)
 Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \ 
-\    ==> Abs_hypreal(hyprel```{X}) + -hypreal_of_real x : Infinitesimal";
+\    ==> Abs_hypreal(hyprel``{X}) + -hypreal_of_real x : Infinitesimal";
 by (auto_tac (claset() addSIs [bexI] 
            addDs [rename_numerals FreeUltrafilterNat_inverse_real_of_posnat,
                   FreeUltrafilterNat_all,FreeUltrafilterNat_Int] 
@@ -2203,21 +2203,21 @@
 qed "real_seq_to_hypreal_Infinitesimal";
 
 Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \ 
-\     ==> Abs_hypreal(hyprel```{X}) @= hypreal_of_real x";
+\     ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x";
 by (rtac (inf_close_minus_iff RS ssubst) 1);
 by (rtac (mem_infmal_iff RS subst) 1);
 by (etac real_seq_to_hypreal_Infinitesimal 1);
 qed "real_seq_to_hypreal_inf_close";
 
 Goal "ALL n. abs(x + -X n) < inverse(real_of_nat(Suc n)) \ 
-\              ==> Abs_hypreal(hyprel```{X}) @= hypreal_of_real x";
+\              ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x";
 by (asm_full_simp_tac (simpset() addsimps [abs_minus_add_cancel,
         real_seq_to_hypreal_inf_close]) 1);
 qed "real_seq_to_hypreal_inf_close2";
 
 Goal "ALL n. abs(X n + -Y n) < inverse(real_of_nat(Suc n)) \ 
-\     ==> Abs_hypreal(hyprel```{X}) + \
-\         -Abs_hypreal(hyprel```{Y}) : Infinitesimal";
+\     ==> Abs_hypreal(hyprel``{X}) + \
+\         -Abs_hypreal(hyprel``{Y}) : Infinitesimal";
 by (auto_tac (claset() addSIs [bexI] 
                   addDs [rename_numerals 
                          FreeUltrafilterNat_inverse_real_of_posnat,
--- a/src/HOL/Hyperreal/NatStar.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/NatStar.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -117,7 +117,7 @@
          simpset()));
 qed "NatStar_mem";
 
-Goalw [starsetNat_def] "hypnat_of_nat `` A <= *sNat* A";
+Goalw [starsetNat_def] "hypnat_of_nat ` A <= *sNat* A";
 by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_def]));
 by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
 qed "NatStar_hypreal_of_real_image_subset";
@@ -128,7 +128,7 @@
 qed "NatStar_SHNat_subset";
 
 Goalw [starsetNat_def] 
-     "*sNat* X Int SNat = hypnat_of_nat `` X";
+     "*sNat* X Int SNat = hypnat_of_nat ` X";
 by (auto_tac (claset(),
          simpset() addsimps 
            [hypnat_of_nat_def,SHNat_def]));
@@ -140,7 +140,7 @@
 by (Auto_tac);
 qed "NatStar_hypreal_of_real_Int";
 
-Goal "x ~: hypnat_of_nat `` A ==> ALL y: A. x ~= hypnat_of_nat y";
+Goal "x ~: hypnat_of_nat ` A ==> ALL y: A. x ~= hypnat_of_nat y";
 by (Auto_tac);
 qed "lemma_not_hypnatA";
 
@@ -188,15 +188,15 @@
 qed "starfunNat2_n_starfunNat2";
 
 Goalw [congruent_def] 
-      "congruent hypnatrel (%X. hypnatrel```{%n. f (X n)})";
+      "congruent hypnatrel (%X. hypnatrel``{%n. f (X n)})";
 by (safe_tac (claset()));
 by (ALLGOALS(Fuf_tac));
 qed "starfunNat_congruent";
 
 (* f::nat=>real *)
 Goalw [starfunNat_def]
-      "(*fNat* f) (Abs_hypnat(hypnatrel```{%n. X n})) = \
-\      Abs_hypreal(hyprel ``` {%n. f (X n)})";
+      "(*fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
+\      Abs_hypreal(hyprel `` {%n. f (X n)})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
 by (simp_tac (simpset() addsimps 
    [hyprel_in_hypreal RS Abs_hypreal_inverse]) 1);
@@ -205,8 +205,8 @@
 
 (* f::nat=>nat *)
 Goalw [starfunNat2_def]
-      "(*fNat2* f) (Abs_hypnat(hypnatrel```{%n. X n})) = \
-\      Abs_hypnat(hypnatrel ``` {%n. f (X n)})";
+      "(*fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
+\      Abs_hypnat(hypnatrel `` {%n. f (X n)})";
 by (res_inst_tac [("f","Abs_hypnat")] arg_cong 1);
 by (simp_tac (simpset() addsimps 
    [hypnatrel_in_hypnat RS Abs_hypnat_inverse,
@@ -413,14 +413,14 @@
      Internal functions - some redundancy with *fNat* now
  ---------------------------------------------------------*)
 Goalw [congruent_def] 
-      "congruent hypnatrel (%X. hypnatrel```{%n. f n (X n)})";
+      "congruent hypnatrel (%X. hypnatrel``{%n. f n (X n)})";
 by (safe_tac (claset()));
 by (ALLGOALS(Fuf_tac));
 qed "starfunNat_n_congruent";
 
 Goalw [starfunNat_n_def]
-     "(*fNatn* f) (Abs_hypnat(hypnatrel```{%n. X n})) = \
-\     Abs_hypreal(hyprel ``` {%n. f n (X n)})";
+     "(*fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
+\     Abs_hypreal(hyprel `` {%n. f n (X n)})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
 by Auto_tac;
 by (Ultra_tac 1);
@@ -468,7 +468,7 @@
 by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus]));
 qed "starfunNat_n_minus";
 
-Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel ``` {%i. f i n})";
+Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
 by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def]));
 qed "starfunNat_n_eq";
 Addsimps [starfunNat_n_eq];
--- a/src/HOL/Hyperreal/NatStar.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/NatStar.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -23,10 +23,10 @@
     (* star transform of functions f:Nat --> Real *)
 
     starfunNat :: (nat => real) => hypnat => hypreal        ("*fNat* _" [80] 80)
-    "*fNat* f  == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel```{%n. f (X n)}))" 
+    "*fNat* f  == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel``{%n. f (X n)}))" 
 
     starfunNat_n :: (nat => (nat => real)) => hypnat => hypreal        ("*fNatn* _" [80] 80)
-    "*fNatn* F  == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel```{%n. (F n)(X n)}))" 
+    "*fNatn* F  == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel``{%n. (F n)(X n)}))" 
 
     InternalNatFuns :: (hypnat => hypreal) set
     "InternalNatFuns == {X. EX F. X = *fNatn* F}"
@@ -34,10 +34,10 @@
     (* star transform of functions f:Nat --> Nat *)
 
     starfunNat2 :: (nat => nat) => hypnat => hypnat        ("*fNat2* _" [80] 80)
-    "*fNat2* f  == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel```{%n. f (X n)}))" 
+    "*fNat2* f  == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel``{%n. f (X n)}))" 
 
     starfunNat2_n :: (nat => (nat => nat)) => hypnat => hypnat        ("*fNat2n* _" [80] 80)
-    "*fNat2n* F  == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel```{%n. (F n)(X n)}))" 
+    "*fNat2n* F  == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel``{%n. (F n)(X n)}))" 
 
     InternalNatFuns2 :: (hypnat => hypnat) set
     "InternalNatFuns2 == {X. EX F. X = *fNat2n* F}"
--- a/src/HOL/Hyperreal/SEQ.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -141,7 +141,7 @@
 
 (* thus, the sequence defines an infinite hypernatural! *)
 Goal "ALL n. n <= f n \
-\         ==> Abs_hypnat (hypnatrel ``` {f}) : HNatInfinite";
+\         ==> Abs_hypnat (hypnatrel `` {f}) : HNatInfinite";
 by (auto_tac (claset(),simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
 by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
 by (etac FreeUltrafilterNat_NSLIMSEQ 1);
@@ -156,7 +156,7 @@
 val lemmaLIM2 = result();
 
 Goal "[| #0 < r; ALL n. r <= abs (X (f n) + - L); \
-\          (*fNat* X) (Abs_hypnat (hypnatrel ``` {f})) + \
+\          (*fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \
 \          - hypreal_of_real  L @= 0 |] ==> False";
 by (auto_tac (claset(),simpset() addsimps [starfunNat,
     mem_infmal_iff RS sym,hypreal_of_real_def,
@@ -178,7 +178,7 @@
 by (Step_tac 1);
 (* skolemization step *)
 by (dtac choice 1 THEN Step_tac 1);
-by (dres_inst_tac [("x","Abs_hypnat(hypnatrel```{f})")] bspec 1);
+by (dres_inst_tac [("x","Abs_hypnat(hypnatrel``{f})")] bspec 1);
 by (dtac (inf_close_minus_iff RS iffD1) 2);
 by (fold_tac [real_le_def]);
 by (blast_tac (claset() addIs [HNatInfinite_NSLIMSEQ]) 1);
@@ -511,7 +511,7 @@
 val lemmaNSBseq2 = result();
 
 Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \
-\         ==>  Abs_hypreal(hyprel```{X o f}) : HInfinite";
+\         ==>  Abs_hypreal(hyprel``{X o f}) : HInfinite";
 by (auto_tac (claset(),
               simpset() addsimps [HInfinite_FreeUltrafilterNat_iff,o_def]));
 by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
@@ -542,7 +542,7 @@
 val lemma_finite_NSBseq2 = result();
 
 Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \
-\     ==> Abs_hypnat(hypnatrel```{f}) : HNatInfinite";
+\     ==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite";
 by (auto_tac (claset(),
               simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
 by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
@@ -795,7 +795,7 @@
 (*-------------------------------
       Standard def => NS def
  -------------------------------*)
-Goal "Abs_hypnat (hypnatrel ``` {x}) : HNatInfinite \
+Goal "Abs_hypnat (hypnatrel `` {x}) : HNatInfinite \
 \         ==> {n. M <= x n} : FreeUltrafilterNat";
 by (auto_tac (claset(),
               simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
@@ -843,7 +843,7 @@
     step_tac (claset() addSDs [all_conj_distrib RS iffD1]) 1);
 by (REPEAT(dtac HNatInfinite_NSLIMSEQ 1));
 by (dtac bspec 1 THEN assume_tac 1);
-by (dres_inst_tac [("x","Abs_hypnat (hypnatrel ``` {fa})")] bspec 1 
+by (dres_inst_tac [("x","Abs_hypnat (hypnatrel `` {fa})")] bspec 1 
     THEN auto_tac (claset(), simpset() addsimps [starfunNat]));
 by (dtac (inf_close_minus_iff RS iffD1) 1);
 by (dtac (mem_infmal_iff RS iffD2) 1);
@@ -1334,7 +1334,7 @@
                  Hyperreals and Sequences
  ---------------------------------------------------------------***)
 (*** A bounded sequence is a finite hyperreal ***)
-Goal "NSBseq X ==> Abs_hypreal(hyprel```{X}) : HFinite";
+Goal "NSBseq X ==> Abs_hypreal(hyprel``{X}) : HFinite";
 by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl] addIs 
        [FreeUltrafilterNat_all RS FreeUltrafilterNat_subset],
        simpset() addsimps [HFinite_FreeUltrafilterNat_iff,
@@ -1343,7 +1343,7 @@
 
 (*** A sequence converging to zero defines an infinitesimal ***)
 Goalw [NSLIMSEQ_def] 
-      "X ----NS> #0 ==> Abs_hypreal(hyprel```{X}) : Infinitesimal";
+      "X ----NS> #0 ==> Abs_hypreal(hyprel``{X}) : Infinitesimal";
 by (dres_inst_tac [("x","whn")] bspec 1);
 by (simp_tac (simpset() addsimps [HNatInfinite_whn]) 1);
 by (auto_tac (claset(),
--- a/src/HOL/Hyperreal/Star.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/Star.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -83,12 +83,12 @@
 by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],simpset()));
 qed "STAR_mem";
 
-Goalw [starset_def] "hypreal_of_real `` A <= *s* A";
+Goalw [starset_def] "hypreal_of_real ` A <= *s* A";
 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def]));
 by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
 qed "STAR_hypreal_of_real_image_subset";
 
-Goalw [starset_def] "*s* X Int SReal = hypreal_of_real `` X";
+Goalw [starset_def] "*s* X Int SReal = hypreal_of_real ` X";
 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,SReal_def]));
 by (fold_tac [hypreal_of_real_def]);
 by (rtac imageI 1 THEN rtac ccontr 1);
@@ -98,7 +98,7 @@
 by (Auto_tac);
 qed "STAR_hypreal_of_real_Int";
 
-Goal "x ~: hypreal_of_real `` A ==> ALL y: A. x ~= hypreal_of_real y";
+Goal "x ~: hypreal_of_real ` A ==> ALL y: A. x ~= hypreal_of_real y";
 by (Auto_tac);
 qed "lemma_not_hyprealA";
 
@@ -108,7 +108,7 @@
 
 Goalw [starset_def]
     "ALL n. (X n) ~: M \
-\         ==> Abs_hypreal(hyprel```{X}) ~: *s* M";
+\         ==> Abs_hypreal(hyprel``{X}) ~: *s* M";
 by (Auto_tac THEN rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
 by (Auto_tac);
 qed "STAR_real_seq_to_hypreal";
@@ -193,14 +193,14 @@
     Nonstandard extension of functions- congruence 
  -----------------------------------------------------------------------*) 
 
-Goalw [congruent_def] "congruent hyprel (%X. hyprel```{%n. f (X n)})";
+Goalw [congruent_def] "congruent hyprel (%X. hyprel``{%n. f (X n)})";
 by (safe_tac (claset()));
 by (ALLGOALS(Fuf_tac));
 qed "starfun_congruent";
 
 Goalw [starfun_def]
-      "(*f* f) (Abs_hypreal(hyprel```{%n. X n})) = \
-\      Abs_hypreal(hyprel ``` {%n. f (X n)})";
+      "(*f* f) (Abs_hypreal(hyprel``{%n. X n})) = \
+\      Abs_hypreal(hyprel `` {%n. f (X n)})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
 by (simp_tac (simpset() addsimps 
    [hyprel_in_hypreal RS Abs_hypreal_inverse,[equiv_hyprel,
@@ -417,8 +417,8 @@
    applied entrywise to equivalence class representative.
    This is easily proved using starfun and ns extension thm
  ------------------------------------------------------------*)
-Goal "abs (Abs_hypreal (hyprel ``` {X})) = \
-\                 Abs_hypreal(hyprel ``` {%n. abs (X n)})";
+Goal "abs (Abs_hypreal (hyprel `` {X})) = \
+\                 Abs_hypreal(hyprel `` {%n. abs (X n)})";
 by (simp_tac (simpset() addsimps [starfun_rabs_hrabs RS sym,starfun]) 1);
 qed "hypreal_hrabs";
 
@@ -470,7 +470,7 @@
 by (Fuf_tac 1);
 qed  "Infinitesimal_FreeUltrafilterNat_iff2";
 
-Goal "(Abs_hypreal(hyprel```{X}) @= Abs_hypreal(hyprel```{Y})) = \
+Goal "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) = \
 \     (ALL m. {n. abs (X n + - Y n) < \
 \                 inverse(real_of_nat(Suc m))} : FreeUltrafilterNat)";
 by (rtac (inf_close_minus_iff RS ssubst) 1);
@@ -485,6 +485,6 @@
 Goal "inj starfun";
 by (rtac injI 1);
 by (rtac ext 1 THEN rtac ccontr 1);
-by (dres_inst_tac [("x","Abs_hypreal(hyprel ```{%n. xa})")] fun_cong 1);
+by (dres_inst_tac [("x","Abs_hypreal(hyprel ``{%n. xa})")] fun_cong 1);
 by (auto_tac (claset(),simpset() addsimps [starfun]));
 qed "inj_starfun";
--- a/src/HOL/Hyperreal/Star.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/Star.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -25,11 +25,11 @@
                         ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
     
     starfun :: (real => real) => hypreal => hypreal        ("*f* _" [80] 80)
-    "*f* f  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel```{%n. f(X n)}))" 
+    "*f* f  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel``{%n. f(X n)}))" 
 
     (* internal functions *)
     starfun_n :: (nat => (real => real)) => hypreal => hypreal        ("*fn* _" [80] 80)
-    "*fn* F  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel```{%n. (F n)(X n)}))" 
+    "*fn* F  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel``{%n. (F n)(X n)}))" 
 
     InternalFuns :: (hypreal => hypreal) set
     "InternalFuns == {X. EX F. X = *fn* F}"
--- a/src/HOL/IMPP/Hoare.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/IMPP/Hoare.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -64,8 +64,8 @@
 by (Fast_tac 1);
 qed "conseq2";
 
-Goal "[| G Un (%p. {P p}.      BODY p  .{Q p})``Procs  \
-\         ||- (%p. {P p}. the (body p) .{Q p})``Procs; \
+Goal "[| G Un (%p. {P p}.      BODY p  .{Q p})`Procs  \
+\         ||- (%p. {P p}. the (body p) .{Q p})`Procs; \
 \   pn:Procs |] ==> G|-{P pn}. BODY pn .{Q pn}";
 bd hoare_derivs.Body 1;
 be hoare_derivs.weaken 1;
@@ -129,7 +129,7 @@
 
 Goal "[| finite U; \
 \ !p. G |-     {P' p}.c0 p.{Q' p}       --> G |-     {P p}.c0 p.{Q p} |] ==> \
-\     G||-(%p. {P' p}.c0 p.{Q' p}) `` U --> G||-(%p. {P p}.c0 p.{Q p}) `` U";
+\     G||-(%p. {P' p}.c0 p.{Q' p}) ` U --> G||-(%p. {P p}.c0 p.{Q p}) ` U";
 be finite_induct 1;
 by (ALLGOALS Clarsimp_tac);
 bd derivs_insertD 1;
@@ -154,9 +154,9 @@
 qed "Loop_sound_lemma";
 
 Goalw [hoare_valids_def]
-   "[| G Un (%pn. {P pn}.      BODY pn  .{Q pn})``Procs \
-\        ||=(%pn. {P pn}. the (body pn) .{Q pn})``Procs |] ==> \
-\       G||=(%pn. {P pn}.      BODY pn  .{Q pn})``Procs";
+   "[| G Un (%pn. {P pn}.      BODY pn  .{Q pn})`Procs \
+\        ||=(%pn. {P pn}. the (body pn) .{Q pn})`Procs |] ==> \
+\       G||=(%pn. {P pn}.      BODY pn  .{Q pn})`Procs";
 br allI 1;
 by (induct_tac "n" 1);
 by  (fast_tac (claset() addIs [Body_triple_valid_0]) 1);
@@ -255,12 +255,12 @@
 \ !!G pn. P (insert (mgt_call pn) G) {mgt(the(body pn))} ==> P G {mgt_call pn};\
 \         !!G c. [| wt c; !pn:U. P G {mgt_call pn} |] ==> P G {mgt c}; \
 \         !!pn. pn : U ==> wt (the (body pn)); \
-\         finite U; uG = mgt_call``U |] ==> \
+\         finite U; uG = mgt_call`U |] ==> \
 \ !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})";
 by (cut_facts_tac (premises()) 1);
 by (induct_tac "n" 1);
 by  (ALLGOALS Clarsimp_tac);
-by  (subgoal_tac "G = mgt_call `` U" 1);
+by  (subgoal_tac "G = mgt_call ` U" 1);
 by   (asm_simp_tac (simpset() addsimps [card_seteq, finite_imageI]) 2);
 by  (Asm_full_simp_tac 1);
 by  (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
@@ -308,9 +308,9 @@
 (* Version: simultaneous recursion in call rule *)
 
 (* finiteness not really necessary here *)
-Goalw [MGT_def]     "[| G Un (%pn. {=}.      BODY pn  .{->})``Procs \
-\                         ||-(%pn. {=}. the (body pn) .{->})``Procs; \
-\ finite Procs |] ==>   G ||-(%pn. {=}.      BODY pn  .{->})``Procs";
+Goalw [MGT_def]     "[| G Un (%pn. {=}.      BODY pn  .{->})`Procs \
+\                         ||-(%pn. {=}. the (body pn) .{->})`Procs; \
+\ finite Procs |] ==>   G ||-(%pn. {=}.      BODY pn  .{->})`Procs";
 br hoare_derivs.Body 1;
 be finite_pointwise 1;
 ba  2;
@@ -321,8 +321,8 @@
 
 (* requires empty, insert, com_det *)
 Goal "[| state_not_singleton; WT_bodies; \
-\ F<=(%pn. {=}.the (body pn).{->})``dom body |] ==> \
-\    (%pn. {=}.     BODY pn .{->})``dom body||-F";
+\ F<=(%pn. {=}.the (body pn).{->})`dom body |] ==> \
+\    (%pn. {=}.     BODY pn .{->})`dom body||-F";
 by (ftac finite_subset 1);
 br  (finite_dom_body RS finite_imageI) 1;
 by (rotate_tac 2 1);
@@ -344,7 +344,7 @@
 ba   1;
 ba  2;
 by (Clarsimp_tac 1);
-by (subgoal_tac "{}||-(%pn. {=}. BODY pn .{->})``dom body" 1);
+by (subgoal_tac "{}||-(%pn. {=}. BODY pn .{->})`dom body" 1);
 be  hoare_derivs.weaken 1;
 by  (fast_tac (claset() addIs [domI]) 1);
 br (finite_dom_body RSN (2,MGT_Body)) 1;
--- a/src/HOL/IMPP/Hoare.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/IMPP/Hoare.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -88,9 +88,9 @@
 	  |-{P}.  the (body pn) .{Q} ==>
 	 G|-{P}.       BODY pn  .{Q}"
 *)
-  Body	"[| G Un (%p. {P p}.      BODY p  .{Q p})``Procs
-	      ||-(%p. {P p}. the (body p) .{Q p})``Procs |]
-	==>  G||-(%p. {P p}.      BODY p  .{Q p})``Procs"
+  Body	"[| G Un (%p. {P p}.      BODY p  .{Q p})`Procs
+	      ||-(%p. {P p}. the (body p) .{Q p})`Procs |]
+	==>  G||-(%p. {P p}.      BODY p  .{Q p})`Procs"
 
   Call	   "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])}
 	==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}.
--- a/src/HOL/Induct/LList.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Induct/LList.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -420,7 +420,7 @@
 \    f(NIL)=g(NIL);                                             \
 \    !!x l. [| x:A;  l: llist(A) |] ==>                         \
 \           (f(CONS x l),g(CONS x l)) :                         \
-\               LListD_Fun (diag A) ((%u.(f(u),g(u)))``llist(A) Un  \
+\               LListD_Fun (diag A) ((%u.(f(u),g(u)))`llist(A) Un  \
 \                                   diag(llist(A)))             \
 \ |] ==> f(M) = g(M)";
 by (rtac LList_equalityI 1);
@@ -461,7 +461,7 @@
 qed "Lmap_type";
 
 (*This type checking rule synthesises a sufficiently large set for f*)
-Goal "M: llist(A) ==> Lmap f M: llist(f``A)";
+Goal "M: llist(A) ==> Lmap f M: llist(f`A)";
 by (etac Lmap_type 1);
 by (etac imageI 1);
 qed "Lmap_type2";
@@ -541,7 +541,7 @@
 
 (*strong co-induction: bisimulation and case analysis on one variable*)
 Goal "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
-by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
+by (res_inst_tac [("X", "(%u. Lappend u N)`llist(A)")] llist_coinduct 1);
 by (etac imageI 1);
 by (rtac image_subsetI 1);
 by (eres_inst_tac [("aa", "x")] llist.elim 1);
@@ -623,21 +623,21 @@
 by (Fast_tac 1);
 qed "LListD_Fun_subset_Times_llist";
 
-Goal "prod_fun Rep_LList Rep_LList `` r <= \
+Goal "prod_fun Rep_LList Rep_LList ` r <= \
 \    (llist(range Leaf)) <*> (llist(range Leaf))";
 by (fast_tac (claset() delrules [image_subsetI]
 		       addIs [Rep_LList RS LListD]) 1);
 qed "subset_Times_llist";
 
 Goal "r <= (llist(range Leaf)) <*> (llist(range Leaf)) ==> \
-\    prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) `` r <= r";
+\    prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) ` r <= r";
 by Safe_tac;
 by (etac (subsetD RS SigmaE2) 1);
 by (assume_tac 1);
 by (asm_simp_tac (simpset() addsimps [LListI RS Abs_LList_inverse]) 1);
 qed "prod_fun_lemma";
 
-Goal "prod_fun Rep_LList  Rep_LList `` range(%x. (x, x)) = \
+Goal "prod_fun Rep_LList  Rep_LList ` range(%x. (x, x)) = \
 \    diag(llist(range Leaf))";
 by (rtac equalityI 1);
 by (Blast_tac 1);
@@ -659,7 +659,7 @@
 Goalw [llistD_Fun_def]
     "[| (l1,l2) : r;  r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
 by (rtac (inj_Rep_LList RS injD) 1);
-by (res_inst_tac [("r", "prod_fun Rep_LList Rep_LList ``r"),
+by (res_inst_tac [("r", "prod_fun Rep_LList Rep_LList `r"),
                   ("A", "range(Leaf)")] 
         LList_equalityI 1);
 by (etac prod_fun_imageI 1);
--- a/src/HOL/Induct/LList.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Induct/LList.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -20,7 +20,7 @@
   llistD_Fun_def
    "llistD_Fun(r) ==    
        {(LNil,LNil)}  Un        
-       (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
+       (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))`r)"
 *)
 
 LList = Main + SList +
@@ -87,9 +87,9 @@
 
   llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
     "llistD_Fun(r) ==    
-        prod_fun Abs_LList Abs_LList ``         
+        prod_fun Abs_LList Abs_LList `         
                 LListD_Fun (diag(range Leaf))   
-                            (prod_fun Rep_LList Rep_LList `` r)"
+                            (prod_fun Rep_LList Rep_LList ` r)"
 
 
 
--- a/src/HOL/Integ/Equiv.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Integ/Equiv.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -37,33 +37,33 @@
 
 (*Lemma for the next result*)
 Goalw [equiv_def,trans_def,sym_def]
-     "[| equiv A r;  (a,b): r |] ==> r```{a} <= r```{b}";
+     "[| equiv A r;  (a,b): r |] ==> r``{a} <= r``{b}";
 by (Blast_tac 1);
 qed "equiv_class_subset";
 
-Goal "[| equiv A r;  (a,b): r |] ==> r```{a} = r```{b}";
+Goal "[| equiv A r;  (a,b): r |] ==> r``{a} = r``{b}";
 by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
 by (rewrite_goals_tac [equiv_def,sym_def]);
 by (Blast_tac 1);
 qed "equiv_class_eq";
 
-Goalw [equiv_def,refl_def] "[| equiv A r;  a: A |] ==> a: r```{a}";
+Goalw [equiv_def,refl_def] "[| equiv A r;  a: A |] ==> a: r``{a}";
 by (Blast_tac 1);
 qed "equiv_class_self";
 
 (*Lemma for the next result*)
 Goalw [equiv_def,refl_def]
-    "[| equiv A r;  r```{b} <= r```{a};  b: A |] ==> (a,b): r";
+    "[| equiv A r;  r``{b} <= r``{a};  b: A |] ==> (a,b): r";
 by (Blast_tac 1);
 qed "subset_equiv_class";
 
-Goal "[| r```{a} = r```{b};  equiv A r;  b: A |] ==> (a,b): r";
+Goal "[| r``{a} = r``{b};  equiv A r;  b: A |] ==> (a,b): r";
 by (REPEAT (ares_tac [equalityD2, subset_equiv_class] 1));
 qed "eq_equiv_class";
 
-(*thus r```{a} = r```{b} as well*)
+(*thus r``{a} = r``{b} as well*)
 Goalw [equiv_def,trans_def,sym_def]
-     "[| equiv A r;  x: (r```{a} Int r```{b}) |] ==> (a,b): r";
+     "[| equiv A r;  x: (r``{a} Int r``{b}) |] ==> (a,b): r";
 by (Blast_tac 1);
 qed "equiv_class_nondisjoint";
 
@@ -71,12 +71,12 @@
 by (Blast_tac 1);
 qed "equiv_type";
 
-Goal "equiv A r ==> ((x,y): r) = (r```{x} = r```{y} & x:A & y:A)";
+Goal "equiv A r ==> ((x,y): r) = (r``{x} = r``{y} & x:A & y:A)";
 by (blast_tac (claset() addSIs [equiv_class_eq]
 	                addDs [eq_equiv_class, equiv_type]) 1);
 qed "equiv_class_eq_iff";
 
-Goal "[| equiv A r;  x: A;  y: A |] ==> (r```{x} = r```{y}) = ((x,y): r)";
+Goal "[| equiv A r;  x: A;  y: A |] ==> (r``{x} = r``{y}) = ((x,y): r)";
 by (blast_tac (claset() addSIs [equiv_class_eq]
 	                addDs [eq_equiv_class, equiv_type]) 1);
 qed "eq_equiv_class_iff";
@@ -85,12 +85,12 @@
 
 (** Introduction/elimination rules -- needed? **)
 
-Goalw [quotient_def] "x:A ==> r```{x}: A//r";
+Goalw [quotient_def] "x:A ==> r``{x}: A//r";
 by (Blast_tac 1);
 qed "quotientI";
 
 val [major,minor] = Goalw [quotient_def]
-    "[| X:(A//r);  !!x. [| X = r```{x};  x:A |] ==> P |]  \
+    "[| X:(A//r);  !!x. [| X = r``{x};  x:A |] ==> P |]  \
 \    ==> P";
 by (resolve_tac [major RS UN_E] 1);
 by (rtac minor 1);
@@ -127,13 +127,13 @@
 
 (*Conversion rule*)
 Goal "[| equiv A r;  congruent r b;  a: A |] \
-\     ==> (UN x:r```{a}. b(x)) = b(a)";
+\     ==> (UN x:r``{a}. b(x)) = b(a)";
 by (rtac (equiv_class_self RS UN_constant_eq) 1 THEN REPEAT (assume_tac 1));
 by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
 by (blast_tac (claset() delrules [equalityI]) 1);
 qed "UN_equiv_class";
 
-(*type checking of  UN x:r``{a}. b(x) *)
+(*type checking of  UN x:r`{a}. b(x) *)
 val prems = Goalw [quotient_def]
     "[| equiv A r;  congruent r b;  X: A//r;     \
 \       !!x.  x : A ==> b(x) : B |]             \
@@ -171,7 +171,7 @@
 
 Goalw [congruent_def]
     "[| equiv A r;  congruent2 r b;  a: A |] ==> \
-\    congruent r (%x1. UN x2:r```{a}. b x1 x2)";
+\    congruent r (%x1. UN x2:r``{a}. b x1 x2)";
 by (Clarify_tac 1);
 by (rtac (equiv_type RS subsetD RS SigmaE2) 1 THEN REPEAT (assume_tac 1));
 by (asm_simp_tac (simpset() addsimps [UN_equiv_class,
@@ -181,7 +181,7 @@
 qed "congruent2_implies_congruent_UN";
 
 Goal "[| equiv A r;  congruent2 r b;  a1: A;  a2: A |]  \
-\    ==> (UN x1:r```{a1}. UN x2:r```{a2}. b x1 x2) = b a1 a2";
+\    ==> (UN x1:r``{a1}. UN x2:r``{a2}. b x1 x2) = b a1 a2";
 by (asm_simp_tac (simpset() addsimps [UN_equiv_class,
                                      congruent2_implies_congruent,
                                      congruent2_implies_congruent_UN]) 1);
--- a/src/HOL/Integ/Equiv.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Integ/Equiv.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -12,7 +12,7 @@
     "equiv A r == refl A r & sym(r) & trans(r)"
 
   quotient :: "['a set, ('a*'a) set] => 'a set set"  (infixl "'/'/" 90) 
-    "A//r == UN x:A. {r```{x}}"      (*set of equiv classes*)
+    "A//r == UN x:A. {r``{x}}"      (*set of equiv classes*)
 
   congruent  :: "[('a*'a) set, 'a=>'b] => bool"
     "congruent r b  == ALL y z. (y,z):r --> b(y)=b(z)"
--- a/src/HOL/Integ/IntDef.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Integ/IntDef.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -23,7 +23,7 @@
 	  [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
 
 Goalw [Integ_def,intrel_def,quotient_def]
-     "intrel```{(x,y)}:Integ";
+     "intrel``{(x,y)}:Integ";
 by (Fast_tac 1);
 qed "intrel_in_integ";
 
@@ -58,18 +58,18 @@
 (**** zminus: unary negation on Integ ****)
 
 Goalw [congruent_def, intrel_def]
-     "congruent intrel (%(x,y). intrel```{(y,x)})";
+     "congruent intrel (%(x,y). intrel``{(y,x)})";
 by (auto_tac (claset(), simpset() addsimps add_ac));
 qed "zminus_congruent";
 
 Goalw [zminus_def]
-      "- Abs_Integ(intrel```{(x,y)}) = Abs_Integ(intrel ``` {(y,x)})";
+      "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})";
 by (simp_tac (simpset() addsimps 
 	      [equiv_intrel RS UN_equiv_class, zminus_congruent]) 1);
 qed "zminus";
 
 (*Every integer can be written in the form Abs_Integ(...) *)
-val [prem] = Goal "(!!x y. z = Abs_Integ(intrel```{(x,y)}) ==> P) ==> P";
+val [prem] = Goal "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P";
 by (res_inst_tac [("x1","z")] 
     (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
 by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
@@ -114,8 +114,8 @@
 (**** zadd: addition on Integ ****)
 
 Goalw [zadd_def]
-  "Abs_Integ(intrel```{(x1,y1)}) + Abs_Integ(intrel```{(x2,y2)}) = \
-\  Abs_Integ(intrel```{(x1+x2, y1+y2)})";
+  "Abs_Integ(intrel``{(x1,y1)}) + Abs_Integ(intrel``{(x2,y2)}) = \
+\  Abs_Integ(intrel``{(x1+x2, y1+y2)})";
 by (asm_simp_tac (simpset() addsimps [UN_UN_split_split_eq]) 1);
 by (stac (equiv_intrel RS UN_equiv_class2) 1);
 by (auto_tac (claset(), simpset() addsimps [congruent2_def]));
@@ -232,7 +232,7 @@
 (*Congruence property for multiplication*)
 Goal "congruent2 intrel \
 \       (%p1 p2. (%(x1,y1). (%(x2,y2).   \
-\                   intrel```{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
+\                   intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
 by (rtac (equiv_intrel RS congruent2_commuteI) 1);
 by (pair_tac "w" 2);
 by (ALLGOALS Clarify_tac);
@@ -249,8 +249,8 @@
 qed "zmult_congruent2";
 
 Goalw [zmult_def]
-   "Abs_Integ((intrel```{(x1,y1)})) * Abs_Integ((intrel```{(x2,y2)})) =   \
-\   Abs_Integ(intrel ``` {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
+   "Abs_Integ((intrel``{(x1,y1)})) * Abs_Integ((intrel``{(x2,y2)})) =   \
+\   Abs_Integ(intrel `` {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
 by (asm_simp_tac
     (simpset() addsimps [UN_UN_split_split_eq, zmult_congruent2,
 			 equiv_intrel RS UN_equiv_class2]) 1);
--- a/src/HOL/Integ/IntDef.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Integ/IntDef.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -19,12 +19,12 @@
 
 defs
   zminus_def
-    "- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel```{(y,x)})"
+    "- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel``{(y,x)})"
 
 constdefs
 
   int :: nat => int
-  "int m == Abs_Integ(intrel ``` {(m,0)})"
+  "int m == Abs_Integ(intrel `` {(m,0)})"
 
   neg   :: int => bool
   "neg(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
@@ -40,7 +40,7 @@
   zadd_def
    "z + w == 
        Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
-		 intrel```{(x1+x2, y1+y2)})"
+		 intrel``{(x1+x2, y1+y2)})"
 
   zdiff_def "z - (w::int) == z + (-w)"
 
@@ -51,6 +51,6 @@
   zmult_def
    "z * w == 
        Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
-		 intrel```{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
+		 intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
 
 end
--- a/src/HOL/Integ/int_arith1.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -436,7 +436,7 @@
     simpset = simpset addsimps add_rules
                       addsimprocs simprocs
                       addcongs [if_weak_cong]}),
-  arith_inj_const ("IntDef.int", HOLogic.natT --> Type("IntDef.int",[])),
+  arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT),
   arith_discrete ("IntDef.int", true)];
 
 end;
--- a/src/HOL/Lattice/Bounds.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lattice/Bounds.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -100,11 +100,11 @@
   by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)
 
 theorem dual_Inf [iff?]:
-    "is_Inf (dual `` A) (dual sup) = is_Sup A sup"
+    "is_Inf (dual ` A) (dual sup) = is_Sup A sup"
   by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)
 
 theorem dual_Sup [iff?]:
-    "is_Sup (dual `` A) (dual inf) = is_Inf A inf"
+    "is_Sup (dual ` A) (dual inf) = is_Inf A inf"
   by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)
 
 
@@ -169,8 +169,8 @@
   assume sup: "is_Sup A sup" and sup': "is_Sup A sup'"
   have "dual sup = dual sup'"
   proof (rule is_Inf_uniq)
-    from sup show "is_Inf (dual `` A) (dual sup)" ..
-    from sup' show "is_Inf (dual `` A) (dual sup')" ..
+    from sup show "is_Inf (dual ` A) (dual sup)" ..
+    from sup' show "is_Inf (dual ` A) (dual sup')" ..
   qed
   thus "sup = sup'" ..
 qed
@@ -268,9 +268,9 @@
 
 theorem is_Sup_binary: "is_Sup {x, y} sup = is_sup x y sup"
 proof -
-  have "is_Sup {x, y} sup = is_Inf (dual `` {x, y}) (dual sup)"
+  have "is_Sup {x, y} sup = is_Inf (dual ` {x, y}) (dual sup)"
     by (simp only: dual_Inf)
-  also have "dual `` {x, y} = {dual x, dual y}"
+  also have "dual ` {x, y} = {dual x, dual y}"
     by simp
   also have "is_Inf \<dots> (dual sup) = is_inf (dual x) (dual y) (dual sup)"
     by (rule is_Inf_binary)
@@ -312,12 +312,12 @@
 theorem Sup_Inf: "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf \<Longrightarrow> is_Inf A inf"
 proof -
   assume "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf"
-  hence "is_Inf (dual `` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
+  hence "is_Inf (dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
     by (simp only: dual_Inf dual_leq)
-  also have "dual `` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual `` A. a' \<sqsubseteq> b'}"
+  also have "dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual ` A. a' \<sqsubseteq> b'}"
     by (auto iff: dual_ball dual_Collect)  (* FIXME !? *)
   finally have "is_Inf \<dots> (dual inf)" .
-  hence "is_Sup (dual `` A) (dual inf)"
+  hence "is_Sup (dual ` A) (dual inf)"
     by (rule Inf_Sup)
   thus ?thesis ..
 qed
--- a/src/HOL/Lattice/CompleteLattice.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -201,8 +201,8 @@
   fix A' :: "'a::complete_lattice dual set"
   show "\<exists>inf'. is_Inf A' inf'"
   proof -
-    have "\<exists>sup. is_Sup (undual `` A') sup" by (rule ex_Sup)
-    hence "\<exists>sup. is_Inf (dual `` undual `` A') (dual sup)" by (simp only: dual_Inf)
+    have "\<exists>sup. is_Sup (undual ` A') sup" by (rule ex_Sup)
+    hence "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
     thus ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
   qed
 qed
@@ -212,17 +212,17 @@
   other.
 *}
 
-theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual `` A)"
+theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual ` A)"
 proof -
-  from is_Inf_Meet have "is_Sup (dual `` A) (dual (\<Sqinter>A))" ..
-  hence "\<Squnion>(dual `` A) = dual (\<Sqinter>A)" ..
+  from is_Inf_Meet have "is_Sup (dual ` A) (dual (\<Sqinter>A))" ..
+  hence "\<Squnion>(dual ` A) = dual (\<Sqinter>A)" ..
   thus ?thesis ..
 qed
 
-theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual `` A)"
+theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual ` A)"
 proof -
-  from is_Sup_Join have "is_Inf (dual `` A) (dual (\<Squnion>A))" ..
-  hence "\<Sqinter>(dual `` A) = dual (\<Squnion>A)" ..
+  from is_Sup_Join have "is_Inf (dual ` A) (dual (\<Squnion>A))" ..
+  hence "\<Sqinter>(dual ` A) = dual (\<Squnion>A)" ..
   thus ?thesis ..
 qed
 
@@ -306,8 +306,8 @@
 theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
 proof -
   assume "A \<subseteq> B"
-  hence "dual `` A \<subseteq> dual `` B" by blast
-  hence "\<Sqinter>(dual `` B) \<sqsubseteq> \<Sqinter>(dual `` A)" by (rule Meet_subset_antimono)
+  hence "dual ` A \<subseteq> dual ` B" by blast
+  hence "\<Sqinter>(dual ` B) \<sqsubseteq> \<Sqinter>(dual ` A)" by (rule Meet_subset_antimono)
   hence "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
   thus ?thesis by (simp only: dual_leq)
 qed
@@ -352,9 +352,9 @@
 
 theorem Join_Un: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
 proof -
-  have "dual (\<Squnion>(A \<union> B)) = \<Sqinter>(dual `` A \<union> dual `` B)"
+  have "dual (\<Squnion>(A \<union> B)) = \<Sqinter>(dual ` A \<union> dual ` B)"
     by (simp only: dual_Join image_Un)
-  also have "\<dots> = \<Sqinter>(dual `` A) \<sqinter> \<Sqinter>(dual `` B)"
+  also have "\<dots> = \<Sqinter>(dual ` A) \<sqinter> \<Sqinter>(dual ` B)"
     by (rule Meet_Un)
   also have "\<dots> = dual (\<Squnion>A \<squnion> \<Squnion>B)"
     by (simp only: dual_join dual_Join)
--- a/src/HOL/Lattice/Orders.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lattice/Orders.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -91,15 +91,15 @@
 lemma dual_equality [iff?]: "(dual x = dual y) = (x = y)"
   by simp
 
-lemma dual_ball [iff?]: "(\<forall>x \<in> A. P (dual x)) = (\<forall>x' \<in> dual `` A. P x')"
+lemma dual_ball [iff?]: "(\<forall>x \<in> A. P (dual x)) = (\<forall>x' \<in> dual ` A. P x')"
 proof
   assume a: "\<forall>x \<in> A. P (dual x)"
-  show "\<forall>x' \<in> dual `` A. P x'"
+  show "\<forall>x' \<in> dual ` A. P x'"
   proof
-    fix x' assume x': "x' \<in> dual `` A"
+    fix x' assume x': "x' \<in> dual ` A"
     have "undual x' \<in> A"
     proof -
-      from x' have "undual x' \<in> undual `` dual `` A" by simp
+      from x' have "undual x' \<in> undual ` dual ` A" by simp
       thus "undual x' \<in> A" by (simp add: image_compose [symmetric])
     qed
     with a have "P (dual (undual x'))" ..
@@ -107,16 +107,16 @@
     finally show "P x'" .
   qed
 next
-  assume a: "\<forall>x' \<in> dual `` A. P x'"
+  assume a: "\<forall>x' \<in> dual ` A. P x'"
   show "\<forall>x \<in> A. P (dual x)"
   proof
     fix x assume "x \<in> A"
-    hence "dual x \<in> dual `` A" by simp
+    hence "dual x \<in> dual ` A" by simp
     with a show "P (dual x)" ..
   qed
 qed
 
-lemma range_dual [simp]: "dual `` UNIV = UNIV"
+lemma range_dual [simp]: "dual ` UNIV = UNIV"
 proof (rule surj_range)
   have "\<And>x'. dual (undual x') = x'" by simp
   thus "surj dual" by (rule surjI)
@@ -124,7 +124,7 @@
 
 lemma dual_all [iff?]: "(\<forall>x. P (dual x)) = (\<forall>x'. P x')"
 proof -
-  have "(\<forall>x \<in> UNIV. P (dual x)) = (\<forall>x' \<in> dual `` UNIV. P x')"
+  have "(\<forall>x \<in> UNIV. P (dual x)) = (\<forall>x' \<in> dual ` UNIV. P x')"
     by (rule dual_ball)
   thus ?thesis by simp
 qed
--- a/src/HOL/Lex/Automata.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/Automata.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -7,7 +7,7 @@
 (*** Equivalence of NA and DA ***)
 
 Goalw [na2da_def]
- "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w `` Q)";
+ "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w ` Q)";
 by (induct_tac "w" 1);
  by Auto_tac;
 qed_spec_mp "DA_delta_is_lift_NA_delta";
@@ -21,7 +21,7 @@
 (*** Direct equivalence of NAe and DA ***)
 
 Goalw [nae2da_def]
- "!Q. (eps A)^* ``` (DA.delta (nae2da A) w Q) = steps A w ``` Q";
+ "!Q. (eps A)^* `` (DA.delta (nae2da A) w Q) = steps A w `` Q";
 by (induct_tac "w" 1);
  by (Simp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [step_def]) 1);
@@ -29,7 +29,7 @@
 qed_spec_mp "espclosure_DA_delta_is_steps";
 
 Goalw [nae2da_def]
- "fin (nae2da A) Q = (? q : (eps A)^* ``` Q. fin A q)";
+ "fin (nae2da A) Q = (? q : (eps A)^* `` Q. fin A q)";
 by (Simp_tac 1);
 val lemma = result();
 
--- a/src/HOL/Lex/Automata.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/Automata.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -10,11 +10,11 @@
 
 constdefs
  na2da :: ('a,'s)na => ('a,'s set)da
-"na2da A == ({start A}, %a Q. Union(next A a `` Q), %Q. ? q:Q. fin A q)"
+"na2da A == ({start A}, %a Q. Union(next A a ` Q), %Q. ? q:Q. fin A q)"
 
  nae2da :: ('a,'s)nae => ('a,'s set)da
 "nae2da A == ({start A},
-              %a Q. Union(next A (Some a) `` ((eps A)^* ``` Q)),
-              %Q. ? p: (eps A)^* ``` Q. fin A p)"
+              %a Q. Union(next A (Some a) ` ((eps A)^* `` Q)),
+              %Q. ? p: (eps A)^* `` Q. fin A p)"
 
 end
--- a/src/HOL/Lex/NA.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/NA.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -13,7 +13,7 @@
 consts delta :: "('a,'s)na => 'a list => 's => 's set"
 primrec
 "delta A []    p = {p}"
-"delta A (a#w) p = Union(delta A w `` next A a p)"
+"delta A (a#w) p = Union(delta A w ` next A a p)"
 
 constdefs
  accepts ::   ('a,'s)na => 'a list => bool
--- a/src/HOL/Lex/NAe.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/NAe.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -39,7 +39,7 @@
 AddIffs [in_steps_append];
 
 (* Equivalence of steps and delta
-(* Use "(? x : f `` A. P x) = (? a:A. P(f x))" ?? *)
+(* Use "(? x : f ` A. P x) = (? a:A. P(f x))" ?? *)
 Goal "!p. (p,q) : steps A w = (q : delta A w p)";
 by (induct_tac "w" 1);
  by (Simp_tac 1);
--- a/src/HOL/Lex/NAe.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/NAe.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -25,7 +25,7 @@
 (* not really used:
 consts delta :: "('a,'s)nae => 'a list => 's => 's set"
 primrec
-"delta A [] s = (eps A)^* ``` {s}"
-"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ``` {s}))"
+"delta A [] s = (eps A)^* `` {s}"
+"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* `` {s}))"
 *)
 end
--- a/src/HOL/Lex/RegExp2NA.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/RegExp2NA.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -12,7 +12,7 @@
 types 'a bitsNA = ('a,bool list)na
 
 syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
-translations "x ## S" == "Cons x `` S"
+translations "x ## S" == "Cons x ` S"
 
 constdefs
  atom  :: 'a => 'a bitsNA
--- a/src/HOL/Lex/RegExp2NAe.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/RegExp2NAe.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -12,7 +12,7 @@
 types 'a bitsNAe = ('a,bool list)nae
 
 syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
-translations "x ## S" == "Cons x `` S"
+translations "x ## S" == "Cons x ` S"
 
 constdefs
  atom  :: 'a => 'a bitsNAe
--- a/src/HOL/MicroJava/BV/JVM.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -187,7 +187,7 @@
   have "set pTs \<subseteq> types G"
     by auto
 
-  hence "OK `` set pTs \<subseteq> err (types G)"
+  hence "OK ` set pTs \<subseteq> err (types G)"
     by auto
 
   with instrs maxr isclass 
@@ -329,7 +329,7 @@
   have "set pTs \<subseteq> types G"
     by auto
 
-  hence "OK `` set pTs \<subseteq> err (types G)"
+  hence "OK ` set pTs \<subseteq> err (types G)"
     by auto
 
   with instrs isclass 
--- a/src/HOL/MicroJava/J/JBasis.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/MicroJava/J/JBasis.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -25,8 +25,8 @@
 
 section "unique";
 
-Goal "(x, y) : set l --> x : fst `` set l";
-by (induct_tac "l" 1);
+Goal "(x, y) : set xys --> x : fst ` set xys";
+by (induct_tac "xys" 1);
 by  Auto_tac;
 qed_spec_mp "fst_in_set_lemma";
 
--- a/src/HOL/NumberTheory/BijectionRel.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/NumberTheory/BijectionRel.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -33,12 +33,12 @@
 val lemma_induct = result();
 
 Goalw [inj_on_def] 
-      "[| A <= B; a ~: A ; a : B; inj_on f B |] ==> (f a) ~: f``A";
+      "[| A <= B; a ~: A ; a : B; inj_on f B |] ==> (f a) ~: f`A";
 by Auto_tac;
 val lemma = result();
 
 Goal "[| ALL a. a:A --> P a (f a); inj_on f A; finite A; F <= A |] \
-\    ==> (F,f``F) : bijR P";
+\    ==> (F,f`F) : bijR P";
 by (res_inst_tac [("F","F"),("A","A")] lemma_induct 1);
 by (rtac finite_subset 1);
 by Auto_tac;
@@ -48,7 +48,7 @@
 val lemma = result();
 
 Goal "[| ALL a. a:A --> P a (f a); inj_on f A; finite A |] \
-\    ==> (A,f``A) : bijR P";
+\    ==> (A,f`A) : bijR P";
 by (rtac lemma 1);
 by Auto_tac;
 qed "inj_func_bijR";
--- a/src/HOL/NumberTheory/EulerFermat.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/NumberTheory/EulerFermat.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -121,7 +121,7 @@
 by Auto_tac;
 qed_spec_mp "RRset_gcd";
 
-Goal "[| A : RsetR m;  #0<m; zgcd(x, m) = #1 |] ==> (%a. a*x)``A : RsetR m";
+Goal "[| A : RsetR m;  #0<m; zgcd(x, m) = #1 |] ==> (%a. a*x)`A : RsetR m";
 by (etac RsetR.induct 1);
 by (ALLGOALS Simp_tac);
 by (rtac RsetR.insert 1);
@@ -196,7 +196,7 @@
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zcong_sym])));
 qed "RRset2norRR_inj";
 
-Goal "[| #1<m; is_RRset A m |] ==> (RRset2norRR A m)``A = (norRRset m)";
+Goal "[| #1<m; is_RRset A m |] ==> (RRset2norRR A m)`A = (norRRset m)";
 by (rtac card_seteq 1);
 by (stac card_image 3);
 by (rtac RRset2norRR_inj 4);
@@ -207,11 +207,11 @@
 by (auto_tac (claset(),simpset() addsimps [RsetR_fin,Bnor_fin]));
 qed "RRset2norRR_eq_norR";
 
-Goalw [inj_on_def] "[| a ~: A ; inj f |] ==> (f a) ~: f``A";
+Goalw [inj_on_def] "[| a ~: A ; inj f |] ==> (f a) ~: f`A";
 by Auto_tac;
 val lemma = result();
 
-Goal "x~=#0 ==> a<m --> setprod ((%a. a*x) `` BnorRset(a,m)) = \
+Goal "x~=#0 ==> a<m --> setprod ((%a. a*x) ` BnorRset(a,m)) = \
 \     setprod (BnorRset(a,m)) * x^card(BnorRset(a,m))";
 by (induct_thm_tac BnorRset_induct "a m" 1);
 by (stac BnorRset_eq 2);
--- a/src/HOL/NumberTheory/EulerFermat.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/NumberTheory/EulerFermat.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -30,7 +30,7 @@
 defs
   norRRset_def "norRRset m   == BnorRset (m-#1,m)"
 
-  noXRRset_def "noXRRset m x == (%a. a*x)``(norRRset m)"
+  noXRRset_def "noXRRset m x == (%a. a*x)`(norRRset m)"
 
   phi_def      "phi m == card (norRRset m)"
 
--- a/src/HOL/NumberTheory/WilsonBij.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/NumberTheory/WilsonBij.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -127,7 +127,7 @@
 by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l1,l2,l3,l4],simpset()));
 qed "inv_inj";
 
-Goal "p : zprime ==> (inv p)``(d22set (p-#2)) = (d22set (p-#2))";
+Goal "p : zprime ==> (inv p)`(d22set (p-#2)) = (d22set (p-#2))";
 by (rtac endo_inj_surj 1);
 by (rtac d22set_fin 1);
 by (etac inv_inj 2);
@@ -141,7 +141,7 @@
 
 Goalw [reciR_def] "p:zprime \
 \    ==> (d22set(p-#2),d22set(p-#2)) : (bijR (reciR p))";
-by (res_inst_tac [("s","(d22set(p-#2),(inv p)``(d22set(p-#2)))")] subst 1);
+by (res_inst_tac [("s","(d22set(p-#2),(inv p)`(d22set(p-#2)))")] subst 1);
 by (asm_simp_tac (simpset() addsimps [inv_d22set_d22set]) 1);
 by (rtac inj_func_bijR 1);
 by (rtac d22set_fin 3);
--- a/src/HOL/Real/PNat.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/PNat.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -6,7 +6,7 @@
 The positive naturals -- proofs mainly as in theory Nat.
 *)
 
-Goal "mono(%X. {1} Un (Suc``X))";
+Goal "mono(%X. {1} Un Suc`X)";
 by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
 qed "pnat_fun_mono";
 
--- a/src/HOL/Real/PNat.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/PNat.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -9,7 +9,7 @@
 PNat = Main +
 
 typedef
-  pnat = "lfp(%X. {1} Un (Suc``X))"   (lfp_def)
+  pnat = "lfp(%X. {1} Un Suc`X)"   (lfp_def)
 
 instance
    pnat :: {ord, plus, times}
--- a/src/HOL/Real/PRat.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/PRat.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -61,7 +61,7 @@
 
 bind_thm ("equiv_ratrel_iff", [equiv_ratrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
 
-Goalw  [prat_def,ratrel_def,quotient_def] "ratrel```{(x,y)}:prat";
+Goalw  [prat_def,ratrel_def,quotient_def] "ratrel``{(x,y)}:prat";
 by (Blast_tac 1);
 qed "ratrel_in_prat";
 
@@ -95,7 +95,7 @@
 qed "inj_prat_of_pnat";
 
 val [prem] = Goal
-    "(!!x y. z = Abs_prat(ratrel```{(x,y)}) ==> P) ==> P";
+    "(!!x y. z = Abs_prat(ratrel``{(x,y)}) ==> P) ==> P";
 by (res_inst_tac [("x1","z")] 
     (rewrite_rule [prat_def] Rep_prat RS quotientE) 1);
 by (dres_inst_tac [("f","Abs_prat")] arg_cong 1);
@@ -106,12 +106,12 @@
 
 (**** qinv: inverse on prat ****)
 
-Goalw [congruent_def] "congruent ratrel (%(x,y). ratrel```{(y,x)})";
+Goalw [congruent_def] "congruent ratrel (%(x,y). ratrel``{(y,x)})";
 by (auto_tac (claset(), simpset() addsimps [pnat_mult_commute]));  
 qed "qinv_congruent";
 
 Goalw [qinv_def]
-      "qinv (Abs_prat(ratrel```{(x,y)})) = Abs_prat(ratrel ``` {(y,x)})";
+      "qinv (Abs_prat(ratrel``{(x,y)})) = Abs_prat(ratrel `` {(y,x)})";
 by (simp_tac (simpset() addsimps 
 	      [equiv_ratrel RS UN_equiv_class, qinv_congruent]) 1);
 qed "qinv";
@@ -145,7 +145,7 @@
 qed "prat_add_congruent2_lemma";
 
 Goal "congruent2 ratrel (%p1 p2.                  \
-\        (%(x1,y1). (%(x2,y2). ratrel```{(x1*y2 + x2*y1, y1*y2)}) p2) p1)";
+\        (%(x1,y1). (%(x2,y2). ratrel``{(x1*y2 + x2*y1, y1*y2)}) p2) p1)";
 by (rtac (equiv_ratrel RS congruent2_commuteI) 1);
 by (auto_tac (claset() delrules [equalityI],
               simpset() addsimps [prat_add_congruent2_lemma]));
@@ -153,8 +153,8 @@
 qed "prat_add_congruent2";
 
 Goalw [prat_add_def]
-   "Abs_prat((ratrel```{(x1,y1)})) + Abs_prat((ratrel```{(x2,y2)})) =   \
-\   Abs_prat(ratrel ``` {(x1*y2 + x2*y1, y1*y2)})";
+   "Abs_prat((ratrel``{(x1,y1)})) + Abs_prat((ratrel``{(x2,y2)})) =   \
+\   Abs_prat(ratrel `` {(x1*y2 + x2*y1, y1*y2)})";
 by (simp_tac (simpset() addsimps [UN_UN_split_split_eq, prat_add_congruent2, 
 				  equiv_ratrel RS UN_equiv_class2]) 1);
 qed "prat_add";
@@ -189,7 +189,7 @@
 
 Goalw [congruent2_def]
     "congruent2 ratrel (%p1 p2.                  \
-\         (%(x1,y1). (%(x2,y2). ratrel```{(x1*x2, y1*y2)}) p2) p1)";
+\         (%(x1,y1). (%(x2,y2). ratrel``{(x1*x2, y1*y2)}) p2) p1)";
 (*Proof via congruent2_commuteI seems longer*)
 by (Clarify_tac 1);
 by (asm_simp_tac (simpset() addsimps [pnat_mult_assoc]) 1);
@@ -200,8 +200,8 @@
 qed "pnat_mult_congruent2";
 
 Goalw [prat_mult_def]
-  "Abs_prat(ratrel```{(x1,y1)}) * Abs_prat(ratrel```{(x2,y2)}) = \
-\  Abs_prat(ratrel```{(x1*x2, y1*y2)})";
+  "Abs_prat(ratrel``{(x1,y1)}) * Abs_prat(ratrel``{(x2,y2)}) = \
+\  Abs_prat(ratrel``{(x1*x2, y1*y2)})";
 by (asm_simp_tac 
     (simpset() addsimps [UN_UN_split_split_eq, pnat_mult_congruent2,
 			 equiv_ratrel RS UN_equiv_class2]) 1);
@@ -389,7 +389,7 @@
 Goal "!(q::prat). EX x. x + x = q";
 by (rtac allI 1);
 by (res_inst_tac [("z","q")] eq_Abs_prat 1);
-by (res_inst_tac [("x","Abs_prat (ratrel ``` {(x, y+y)})")] exI 1);
+by (res_inst_tac [("x","Abs_prat (ratrel `` {(x, y+y)})")] exI 1);
 by (auto_tac (claset(),
 	      simpset() addsimps 
               [prat_add,pnat_mult_assoc RS sym,pnat_add_mult_distrib,
@@ -398,7 +398,7 @@
 
 Goal "EX (x::prat). x + x = q";
 by (res_inst_tac [("z","q")] eq_Abs_prat 1);
-by (res_inst_tac [("x","Abs_prat (ratrel ``` {(x, y+y)})")] exI 1);
+by (res_inst_tac [("x","Abs_prat (ratrel `` {(x, y+y)})")] exI 1);
 by (auto_tac (claset(),simpset() addsimps 
               [prat_add,pnat_mult_assoc RS sym,pnat_add_mult_distrib,
                pnat_add_mult_distrib2]));
@@ -454,7 +454,7 @@
 
 (* lemma for proving $< is linear *)
 Goalw [prat_def,prat_less_def] 
-      "ratrel ``` {(x, y * ya)} : {p::(pnat*pnat).True}//ratrel";
+      "ratrel `` {(x, y * ya)} : {p::(pnat*pnat).True}//ratrel";
 by (asm_full_simp_tac (simpset() addsimps [ratrel_def,quotient_def]) 1);
 by (Blast_tac 1);
 qed "lemma_prat_less_linear";
@@ -470,15 +470,15 @@
 by (cut_inst_tac  [("z1.0","x*ya"), ("z2.0","xa*y")] pnat_linear_Ex_eq 1);
 by (EVERY1[etac disjE,etac exE]);
 by (eres_inst_tac 
-    [("x","Abs_prat(ratrel```{(xb,ya*y)})")] allE 1);
+    [("x","Abs_prat(ratrel``{(xb,ya*y)})")] allE 1);
 by (asm_full_simp_tac 
     (simpset() addsimps [prat_add, pnat_mult_assoc 
      RS sym,pnat_add_mult_distrib RS sym]) 1);
 by (EVERY1[asm_full_simp_tac (simpset() addsimps pnat_mult_ac),
     etac disjE, assume_tac, etac exE]);
-by (thin_tac "!T. Abs_prat (ratrel ``` {(x, y)}) + T ~= \
-\     Abs_prat (ratrel ``` {(xa, ya)})" 1);
-by (eres_inst_tac [("x","Abs_prat(ratrel```{(xb,y*ya)})")] allE 1);
+by (thin_tac "!T. Abs_prat (ratrel `` {(x, y)}) + T ~= \
+\     Abs_prat (ratrel `` {(xa, ya)})" 1);
+by (eres_inst_tac [("x","Abs_prat(ratrel``{(xb,y*ya)})")] allE 1);
 by (asm_full_simp_tac (simpset() addsimps [prat_add,
       pnat_mult_assoc RS sym,pnat_add_mult_distrib RS sym]) 1);
 by (asm_full_simp_tac (simpset() addsimps pnat_mult_ac) 1);
@@ -696,12 +696,12 @@
 
 (*** lemmas required for lemma_gleason9_34 in PReal : w*y > y/z ***)
 Goalw [prat_of_pnat_def] 
-      "Abs_prat(ratrel```{(x,y)}) = (prat_of_pnat x)*qinv(prat_of_pnat y)";
+      "Abs_prat(ratrel``{(x,y)}) = (prat_of_pnat x)*qinv(prat_of_pnat y)";
 by (auto_tac (claset(),simpset() addsimps [prat_mult,qinv,pnat_mult_1_left,
     pnat_mult_1]));
 qed "Abs_prat_mult_qinv";
 
-Goal "Abs_prat(ratrel```{(x,y)}) <= Abs_prat(ratrel```{(x,Abs_pnat 1)})";
+Goal "Abs_prat(ratrel``{(x,y)}) <= Abs_prat(ratrel``{(x,Abs_pnat 1)})";
 by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
 by (rtac prat_mult_left_le2_mono1 1);
 by (rtac qinv_prat_le 1);
@@ -713,7 +713,7 @@
     pSuc_is_plus_one,pnat_one_def,prat_of_pnat_add]));
 qed "lemma_Abs_prat_le1";
 
-Goal "Abs_prat(ratrel```{(x,Abs_pnat 1)}) <= Abs_prat(ratrel```{(x*y,Abs_pnat 1)})";
+Goal "Abs_prat(ratrel``{(x,Abs_pnat 1)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1)})";
 by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
 by (rtac prat_mult_le2_mono1 1);
 by (pnat_ind_tac "y" 1);
@@ -726,19 +726,19 @@
 			prat_of_pnat_add,prat_of_pnat_mult]));
 qed "lemma_Abs_prat_le2";
 
-Goal "Abs_prat(ratrel```{(x,z)}) <= Abs_prat(ratrel```{(x*y,Abs_pnat 1)})";
+Goal "Abs_prat(ratrel``{(x,z)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1)})";
 by (fast_tac (claset() addIs [prat_le_trans,
 			      lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1);
 qed "lemma_Abs_prat_le3";
 
-Goal "Abs_prat(ratrel```{(x*y,Abs_pnat 1)}) * Abs_prat(ratrel```{(w,x)}) = \
-\         Abs_prat(ratrel```{(w*y,Abs_pnat 1)})";
+Goal "Abs_prat(ratrel``{(x*y,Abs_pnat 1)}) * Abs_prat(ratrel``{(w,x)}) = \
+\         Abs_prat(ratrel``{(w*y,Abs_pnat 1)})";
 by (full_simp_tac (simpset() addsimps [prat_mult,
     pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac) 1);
 qed "pre_lemma_gleason9_34";
 
-Goal "Abs_prat(ratrel```{(y*x,Abs_pnat 1*y)}) = \
-\         Abs_prat(ratrel```{(x,Abs_pnat 1)})";
+Goal "Abs_prat(ratrel``{(y*x,Abs_pnat 1*y)}) = \
+\         Abs_prat(ratrel``{(x,Abs_pnat 1)})";
 by (auto_tac (claset(),
 	      simpset() addsimps [pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac));
 qed "pre_lemma_gleason9_34b";
--- a/src/HOL/Real/PRat.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/PRat.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -20,20 +20,20 @@
 constdefs
 
   prat_of_pnat :: pnat => prat           
-  "prat_of_pnat m == Abs_prat(ratrel```{(m,Abs_pnat 1)})"
+  "prat_of_pnat m == Abs_prat(ratrel``{(m,Abs_pnat 1)})"
 
   qinv      :: prat => prat
-  "qinv(Q)  == Abs_prat(UN (x,y):Rep_prat(Q). ratrel```{(y,x)})" 
+  "qinv(Q)  == Abs_prat(UN (x,y):Rep_prat(Q). ratrel``{(y,x)})" 
 
 defs
 
   prat_add_def  
   "P + Q == Abs_prat(UN (x1,y1):Rep_prat(P). UN (x2,y2):Rep_prat(Q).
-		     ratrel```{(x1*y2 + x2*y1, y1*y2)})"
+		     ratrel``{(x1*y2 + x2*y1, y1*y2)})"
 
   prat_mult_def  
   "P * Q == Abs_prat(UN (x1,y1):Rep_prat(P). UN (x2,y2):Rep_prat(Q).
-		     ratrel```{(x1*x2, y1*y2)})"
+		     ratrel``{(x1*x2, y1*y2)})"
  
   (*** Gleason p. 119 ***)
   prat_less_def
--- a/src/HOL/Real/PReal.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/PReal.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -582,10 +582,10 @@
    prat_of_pnat_add,prat_add_assoc RS sym]));
 qed "lemma1_gleason9_34";
 
-Goal "Abs_prat (ratrel ``` {(y, z)}) < xb + \
-\         Abs_prat (ratrel ``` {(x*y, Abs_pnat 1)})*Abs_prat (ratrel ``` {(w, x)})";
-by (res_inst_tac [("j","Abs_prat (ratrel ``` {(x * y, Abs_pnat 1)}) *\
-\                   Abs_prat (ratrel ``` {(w, x)})")] prat_le_less_trans 1);
+Goal "Abs_prat (ratrel `` {(y, z)}) < xb + \
+\         Abs_prat (ratrel `` {(x*y, Abs_pnat 1)})*Abs_prat (ratrel `` {(w, x)})";
+by (res_inst_tac [("j","Abs_prat (ratrel `` {(x * y, Abs_pnat 1)}) *\
+\                   Abs_prat (ratrel `` {(w, x)})")] prat_le_less_trans 1);
 by (rtac prat_self_less_add_right 2);
 by (auto_tac (claset() addIs [lemma_Abs_prat_le3],
     simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc]));
--- a/src/HOL/Real/RealDef.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/RealDef.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -57,11 +57,11 @@
                        addSEs [sym, preal_trans_lemma]) 1);
 qed "equiv_realrel";
 
-(* (realrel ``` {x} = realrel ``` {y}) = ((x,y) : realrel) *)
+(* (realrel `` {x} = realrel `` {y}) = ((x,y) : realrel) *)
 bind_thm ("equiv_realrel_iff",
     	  [equiv_realrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
 
-Goalw  [real_def,realrel_def,quotient_def] "realrel```{(x,y)}:real";
+Goalw  [real_def,realrel_def,quotient_def] "realrel``{(x,y)}:real";
 by (Blast_tac 1);
 qed "realrel_in_real";
 
@@ -95,7 +95,7 @@
 qed "inj_real_of_preal";
 
 val [prem] = Goal
-    "(!!x y. z = Abs_real(realrel```{(x,y)}) ==> P) ==> P";
+    "(!!x y. z = Abs_real(realrel``{(x,y)}) ==> P) ==> P";
 by (res_inst_tac [("x1","z")] 
     (rewrite_rule [real_def] Rep_real RS quotientE) 1);
 by (dres_inst_tac [("f","Abs_real")] arg_cong 1);
@@ -107,13 +107,13 @@
 (**** real_minus: additive inverse on real ****)
 
 Goalw [congruent_def]
-  "congruent realrel (%p. (%(x,y). realrel```{(y,x)}) p)";
+  "congruent realrel (%p. (%(x,y). realrel``{(y,x)}) p)";
 by (Clarify_tac 1); 
 by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
 qed "real_minus_congruent";
 
 Goalw [real_minus_def]
-      "- (Abs_real(realrel```{(x,y)})) = Abs_real(realrel ``` {(y,x)})";
+      "- (Abs_real(realrel``{(x,y)})) = Abs_real(realrel `` {(y,x)})";
 by (res_inst_tac [("f","Abs_real")] arg_cong 1);
 by (simp_tac (simpset() addsimps 
    [realrel_in_real RS Abs_real_inverse,
@@ -150,7 +150,7 @@
 (*** Congruence property for addition ***)
 Goalw [congruent2_def]
     "congruent2 realrel (%p1 p2.                  \
-\         (%(x1,y1). (%(x2,y2). realrel```{(x1+x2, y1+y2)}) p2) p1)";
+\         (%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)";
 by (Clarify_tac 1); 
 by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1);
 by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1);
@@ -159,8 +159,8 @@
 qed "real_add_congruent2";
 
 Goalw [real_add_def]
-  "Abs_real(realrel```{(x1,y1)}) + Abs_real(realrel```{(x2,y2)}) = \
-\  Abs_real(realrel```{(x1+x2, y1+y2)})";
+  "Abs_real(realrel``{(x1,y1)}) + Abs_real(realrel``{(x2,y2)}) = \
+\  Abs_real(realrel``{(x1+x2, y1+y2)})";
 by (simp_tac (simpset() addsimps 
               [[equiv_realrel, real_add_congruent2] MRS UN_equiv_class2]) 1);
 qed "real_add";
@@ -301,7 +301,7 @@
 
 Goal 
     "congruent2 realrel (%p1 p2.                  \
-\         (%(x1,y1). (%(x2,y2). realrel```{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)";
+\         (%(x1,y1). (%(x2,y2). realrel``{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)";
 by (rtac (equiv_realrel RS congruent2_commuteI) 1);
 by (Clarify_tac 1); 
 by (rewtac split_def);
@@ -310,8 +310,8 @@
 qed "real_mult_congruent2";
 
 Goalw [real_mult_def]
-   "Abs_real((realrel```{(x1,y1)})) * Abs_real((realrel```{(x2,y2)})) =   \
-\   Abs_real(realrel ``` {(x1*x2+y1*y2,x1*y2+x2*y1)})";
+   "Abs_real((realrel``{(x1,y1)})) * Abs_real((realrel``{(x2,y2)})) =   \
+\   Abs_real(realrel `` {(x1*x2+y1*y2,x1*y2+x2*y1)})";
 by (simp_tac (simpset() addsimps
                [[equiv_realrel, real_mult_congruent2] MRS UN_equiv_class2]) 1);
 qed "real_mult";
@@ -451,7 +451,7 @@
 
 (*** existence of inverse ***)
 (** lemma -- alternative definition of 0 **)
-Goalw [real_zero_def] "0 = Abs_real (realrel ``` {(x, x)})";
+Goalw [real_zero_def] "0 = Abs_real (realrel `` {(x, x)})";
 by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
 qed "real_zero_iff";
 
@@ -461,10 +461,10 @@
 by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1);
 by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
            simpset() addsimps [real_zero_iff RS sym]));
-by (res_inst_tac [("x","Abs_real (realrel ``` \
+by (res_inst_tac [("x","Abs_real (realrel `` \
 \   {(preal_of_prat(prat_of_pnat 1p),pinv(D)+\
 \    preal_of_prat(prat_of_pnat 1p))})")] exI 1);
-by (res_inst_tac [("x","Abs_real (realrel ``` \
+by (res_inst_tac [("x","Abs_real (realrel `` \
 \   {(pinv(D)+preal_of_prat(prat_of_pnat 1p),\
 \    preal_of_prat(prat_of_pnat 1p))})")] exI 2);
 by (auto_tac (claset(),
@@ -716,13 +716,13 @@
 
 Goalw [real_of_preal_def]
       "!!(x::preal). y < x ==> \
-\      EX m. Abs_real (realrel ``` {(x,y)}) = real_of_preal m";
+\      EX m. Abs_real (realrel `` {(x,y)}) = real_of_preal m";
 by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
     simpset() addsimps preal_add_ac));
 qed "real_of_preal_ExI";
 
 Goalw [real_of_preal_def]
-      "!!(x::preal). EX m. Abs_real (realrel ``` {(x,y)}) = \
+      "!!(x::preal). EX m. Abs_real (realrel `` {(x,y)}) = \
 \                    real_of_preal m ==> y < x";
 by (auto_tac (claset(),
 	      simpset() addsimps 
@@ -731,7 +731,7 @@
     [preal_add_assoc RS sym,preal_self_less_add_left]) 1);
 qed "real_of_preal_ExD";
 
-Goal "(EX m. Abs_real (realrel ``` {(x,y)}) = real_of_preal m) = (y < x)";
+Goal "(EX m. Abs_real (realrel `` {(x,y)}) = real_of_preal m) = (y < x)";
 by (blast_tac (claset() addSIs [real_of_preal_ExI,real_of_preal_ExD]) 1);
 qed "real_of_preal_iff";
 
--- a/src/HOL/Real/RealDef.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/RealDef.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -31,14 +31,14 @@
 defs
 
   real_zero_def  
-  "0 == Abs_real(realrel```{(preal_of_prat(prat_of_pnat 1p),
+  "0 == Abs_real(realrel``{(preal_of_prat(prat_of_pnat 1p),
                                 preal_of_prat(prat_of_pnat 1p))})"
   real_one_def   
-  "1r == Abs_real(realrel```{(preal_of_prat(prat_of_pnat 1p) + 
+  "1r == Abs_real(realrel``{(preal_of_prat(prat_of_pnat 1p) + 
             preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})"
 
   real_minus_def
-  "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel```{(y,x)})"
+  "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel``{(y,x)})"
 
   real_diff_def
   "R - (S::real) == R + - S"
@@ -53,7 +53,7 @@
 
   real_of_preal :: preal => real            
   "real_of_preal m     ==
-           Abs_real(realrel```{(m+preal_of_prat(prat_of_pnat 1p),
+           Abs_real(realrel``{(m+preal_of_prat(prat_of_pnat 1p),
                                preal_of_prat(prat_of_pnat 1p))})"
 
   real_of_posnat :: nat => real             
@@ -66,11 +66,11 @@
 
   real_add_def  
   "P+Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
-                   (%(x1,y1). (%(x2,y2). realrel```{(x1+x2, y1+y2)}) p2) p1)"
+                   (%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)"
   
   real_mult_def  
   "P*Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
-                   (%(x1,y1). (%(x2,y2). realrel```{(x1*x2+y1*y2,x1*y2+x2*y1)})
+                   (%(x1,y1). (%(x2,y2). realrel``{(x1*x2+y1*y2,x1*y2+x2*y1)})
 		   p2) p1)"
 
   real_less_def
--- a/src/HOL/Real/RealInt.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/RealInt.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -7,7 +7,7 @@
 
 
 Goalw [congruent_def]
-  "congruent intrel (%p. (%(i,j). realrel ``` \
+  "congruent intrel (%p. (%(i,j). realrel `` \
 \  {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \
 \    preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)";
 by (auto_tac (claset(),
@@ -16,8 +16,8 @@
 qed "real_of_int_congruent";
 
 Goalw [real_of_int_def]
-   "real_of_int (Abs_Integ (intrel ``` {(i, j)})) = \
-\     Abs_real(realrel ``` \
+   "real_of_int (Abs_Integ (intrel `` {(i, j)})) = \
+\     Abs_real(realrel `` \
 \       {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \
 \         preal_of_prat (prat_of_pnat (pnat_of_nat j)))})";
 by (res_inst_tac [("f","Abs_real")] arg_cong 1);
--- a/src/HOL/Real/RealInt.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/RealInt.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -9,7 +9,7 @@
 
 constdefs 
    real_of_int :: int => real
-   "real_of_int z == Abs_real(UN (i,j): Rep_Integ z. realrel ```
+   "real_of_int z == Abs_real(UN (i,j): Rep_Integ z. realrel ``
                      {(preal_of_prat(prat_of_pnat(pnat_of_nat i)),
                        preal_of_prat(prat_of_pnat(pnat_of_nat j)))})"
 
--- a/src/HOL/UNITY/Channel.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Channel.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -23,7 +23,7 @@
 by Auto_tac;
 qed_spec_mp "minSet_nonempty";
 
-Goal "F : (minSet -`` {Some x}) leadsTo (minSet -`` (Some``greaterThan x))";
+Goal "F : (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))";
 by (rtac leadsTo_weaken 1);
 by (res_inst_tac [("x1","x")] ([UC2, UC1] MRS psp) 1);
 by Safe_tac;
@@ -32,7 +32,7 @@
 qed "minSet_greaterThan";
 
 (*The induction*)
-Goal "F : (UNIV-{{}}) leadsTo (minSet -`` (Some``atLeast y))";
+Goal "F : (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))";
 by (rtac leadsTo_weaken_R 1);
 by (res_inst_tac  [("l", "y"), ("f", "the o minSet"), ("B", "{}")]
      greaterThan_bounded_induct 1);
--- a/src/HOL/UNITY/Channel.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Channel.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -21,10 +21,10 @@
 
 rules
 
-  UC1  "F : (minSet -`` {Some x}) co (minSet -`` (Some``atLeast x))"
+  UC1  "F : (minSet -` {Some x}) co (minSet -` (Some`atLeast x))"
 
   (*  UC1  "F : {s. minSet s = x} co {s. x <= minSet s}"  *)
 
-  UC2  "F : (minSet -`` {Some x}) leadsTo {s. x ~: s}"
+  UC2  "F : (minSet -` {Some x}) leadsTo {s. x ~: s}"
 
 end
--- a/src/HOL/UNITY/ELT.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/ELT.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -15,7 +15,7 @@
 
 Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
 by Safe_tac;
-by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
+by (res_inst_tac [("x", "v ` ?u")] image_eqI 2);
 by Auto_tac;
 qed "givenBy_eq_all";
 
@@ -307,7 +307,7 @@
 (*??IS THIS NEEDED?? or is it just an example of what's provable??*)
 Goal "[| F: (A leadsTo[givenBy v] B);  G : preserves v;  \
 \        F Join G : stable C |] \
-\     ==> F Join G : ((C Int A) leadsTo[(%D. C Int D) `` givenBy v] B)";
+\     ==> F Join G : ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)";
 by (etac leadsETo_induct 1);
 by (stac Int_Union 3);
 by (blast_tac (claset() addIs [leadsETo_UN]) 3);
@@ -368,7 +368,7 @@
 
 Goalw [LeadsETo_def]
      "A LeadsTo[CC] B = \
-\       {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) `` CC] \
+\       {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] \
 \       (reachable F Int B)}";
 by (blast_tac (claset() addDs [e_psp_stable2] addIs [leadsETo_weaken]) 1);
 qed "LeadsETo_eq_leadsETo";
@@ -467,7 +467,7 @@
 
 (*givenBy laws that need to be in the locale*)
 
-Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
+Goal "givenBy (v o f) = extend_set h ` (givenBy v)";
 by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
 by (Deepen_tac 0 1);
 qed "givenBy_o_eq_extend_set";
@@ -483,7 +483,7 @@
 qed "extend_set_givenBy_I";
 
 Goal "F : A leadsTo[CC] B \
-\     ==> extend h F : (extend_set h A) leadsTo[extend_set h `` CC] \
+\     ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC] \
 \                      (extend_set h B)";
 by (etac leadsETo_induct 1);
 by (asm_simp_tac (simpset() addsimps [leadsETo_UN, extend_set_Union]) 3);
@@ -531,11 +531,11 @@
 qed "preserves_o_project_transient_empty";
 
 Goal "[| extend h F Join G : stable C;  \
-\        F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)``givenBy v] B;  \
+\        F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B;  \
 \        G : preserves (v o f) |] \
 \     ==> extend h F Join G : \
 \           (C Int extend_set h (project_set h C Int A)) \
-\           leadsTo[(%D. C Int extend_set h D)``givenBy v]  (extend_set h B)";
+\           leadsTo[(%D. C Int extend_set h D)`givenBy v]  (extend_set h B)";
 by (etac leadsETo_induct 1);
 by (asm_simp_tac (simpset() delsimps UN_simps
 		  addsimps [Int_UN_distrib, leadsETo_UN, extend_set_Union]) 3);
@@ -560,10 +560,10 @@
 Goal "[| extend h F Join G : stable C;  \
 \        F Join project h C G : \
 \            (project_set h C Int A) \
-\            leadsTo[(%D. project_set h C Int D)``givenBy v] B;  \
+\            leadsTo[(%D. project_set h C Int D)`givenBy v] B;  \
 \        G : preserves (v o f) |] \
 \     ==> extend h F Join G : (C Int extend_set h A) \
-\           leadsTo[(%D. C Int extend_set h D)``givenBy v] (extend_set h B)";
+\           leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)";
 by (rtac (lemma RS leadsETo_weaken) 1);
 by (auto_tac (claset(), 
 	      simpset() addsimps [split_extended_all]));
@@ -630,7 +630,7 @@
 
 Goal "[| extend h F Join G : stable C;  \
 \        extend h F Join G : \
-\          (C Int A) leadsTo[(%D. C Int D)``givenBy f]  B |]  \
+\          (C Int A) leadsTo[(%D. C Int D)`givenBy f]  B |]  \
 \ ==> F Join project h C G  \
 \   : (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)";
 by (etac leadsETo_induct 1);
--- a/src/HOL/UNITY/ELT.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/ELT.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -44,7 +44,7 @@
   
   (*the set of all sets determined by f alone*)
   givenBy :: "['a => 'b] => 'a set set"
-    "givenBy f == range (%B. f-`` B)"
+    "givenBy f == range (%B. f-` B)"
 
   (*visible version of the LEADS-TO relation*)
   leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
@@ -54,6 +54,6 @@
   LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
                                         ("(3_/ LeadsTo[_]/ _)" [80,0,80] 80)
     "LeadsETo A CC B ==
-      {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) `` CC] B}"
+      {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] B}"
 
 end
--- a/src/HOL/UNITY/Extend.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Extend.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -50,7 +50,7 @@
 
 Goalw [Restrict_def, image_def]
      "[| s : RR;  Restrict A r = Restrict A s |] \
-\     ==> Restrict A r : Restrict A `` RR";
+\     ==> Restrict A r : Restrict A ` RR";
 by Auto_tac;
 qed "Restrict_imageI";
 
@@ -58,14 +58,14 @@
 by (Blast_tac 1);
 qed "Domain_Restrict";
 
-Goal "(Restrict A r) ``` B = r ``` (A Int B)";
+Goal "(Restrict A r) `` B = r `` (A Int B)";
 by (Blast_tac 1);
 qed "Image_Restrict";
 
 Addsimps [Domain_Restrict, Image_Restrict];
 
 
-Goal "f Id = Id ==> insert Id (f``Acts F) = f `` Acts F";
+Goal "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F";
 by (blast_tac (claset() addIs [sym RS image_eqI]) 1);
 qed "insert_Id_image_Acts";
 
@@ -211,7 +211,7 @@
 (*** project_set: basic properties ***)
 
 (*project_set is simply image!*)
-Goal "project_set h C = f `` C";
+Goal "project_set h C = f ` C";
 by (auto_tac (claset() addIs [f_h_eq RS sym], 
 	      simpset() addsimps [split_extended_all]));
 qed "project_set_eq";
@@ -308,7 +308,7 @@
 qed "inj_extend_act";
 
 Goalw [extend_set_def, extend_act_def]
-     "extend_act h act ``` (extend_set h A) = extend_set h (act ``` A)";
+     "extend_act h act `` (extend_set h A) = extend_set h (act `` A)";
 by (Force_tac 1);
 qed "extend_act_Image";
 Addsimps [extend_act_Image];
@@ -363,17 +363,17 @@
 qed "Init_project";
 Addsimps [Init_project];
 
-Goal "Acts (extend h F) = (extend_act h `` Acts F)";
+Goal "Acts (extend h F) = (extend_act h ` Acts F)";
 by (simp_tac (simpset() addsimps [extend_def, insert_Id_image_Acts]) 1);
 qed "Acts_extend";
 Addsimps [Acts_extend];
 
-Goal "AllowedActs (extend h F) = project_act h -`` AllowedActs F";
+Goal "AllowedActs (extend h F) = project_act h -` AllowedActs F";
 by (simp_tac (simpset() addsimps [extend_def, insert_absorb]) 1);
 qed "AllowedActs_extend";
 Addsimps [AllowedActs_extend];
 
-Goal "Acts(project h C F) = insert Id (project_act h `` Restrict C `` Acts F)";
+Goal "Acts(project h C F) = insert Id (project_act h ` Restrict C ` Acts F)";
 by (auto_tac (claset(), 
 	      simpset() addsimps [project_def, image_iff]));
 qed "Acts_project";
@@ -381,7 +381,7 @@
 
 Goal "AllowedActs(project h C F) = \
 \       {act. Restrict (project_set h C) act \
-\              : project_act h `` Restrict C `` AllowedActs F}";
+\              : project_act h ` Restrict C ` AllowedActs F}";
 by (simp_tac (simpset() addsimps [project_def, image_iff]) 1);
 by (stac insert_absorb 1);
 by (auto_tac (claset() addSIs [inst "x" "Id" bexI], 
@@ -389,7 +389,7 @@
 qed "AllowedActs_project";
 Addsimps [AllowedActs_project];
 
-Goal "Allowed (extend h F) = project h UNIV -`` Allowed F";
+Goal "Allowed (extend h F) = project h UNIV -` Allowed F";
 by (simp_tac (simpset() addsimps [AllowedActs_extend, Allowed_def]) 1);
 by (Blast_tac 1); 
 qed "Allowed_extend";
@@ -422,8 +422,8 @@
 qed "project_act_Restrict_Id_eq";
 
 Goal "project h C (extend h F) = \
-\     mk_program (Init F, Restrict (project_set h C) `` Acts F, \
-\                 {act. Restrict (project_set h C) act : project_act h `` Restrict C `` (project_act h -`` AllowedActs F)})";
+\     mk_program (Init F, Restrict (project_set h C) ` Acts F, \
+\                 {act. Restrict (project_set h C) act : project_act h ` Restrict C ` (project_act h -` AllowedActs F)})";
 by (rtac program_equalityI 1);
 by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 2);
 by (Simp_tac 1);
@@ -761,14 +761,14 @@
 qed "OK_extend_iff";
 
 Goal "F : X guarantees Y ==> \
-\     extend h F : (extend h `` X) guarantees (extend h `` Y)";
+\     extend h F : (extend h ` X) guarantees (extend h ` Y)";
 by (rtac guaranteesI 1);
 by (Clarify_tac 1);
 by (blast_tac (claset() addDs [ok_extend_imp_ok_project, 
                                extend_Join_eq_extend_D, guaranteesD]) 1);
 qed "guarantees_imp_extend_guarantees";
 
-Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
+Goal "extend h F : (extend h ` X) guarantees (extend h ` Y) \
 \     ==> F : X guarantees Y";
 by (auto_tac (claset(), simpset() addsimps [guar_def]));
 by (dres_inst_tac [("x", "extend h G")] spec 1);
@@ -778,7 +778,7 @@
                          inj_extend RS inj_image_mem_iff]) 1);
 qed "extend_guarantees_imp_guarantees";
 
-Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
+Goal "(extend h F : (extend h ` X) guarantees (extend h ` Y)) = \
 \    (F : X guarantees Y)";
 by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
 			       extend_guarantees_imp_guarantees]) 1);
--- a/src/HOL/UNITY/Extend.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Extend.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -21,7 +21,7 @@
      (*Using the locale constant "f", this is  f (h (x,y))) = x*)
   
   extend_set :: "['a*'b => 'c, 'a set] => 'c set"
-    "extend_set h A == h `` (A <*> UNIV)"
+    "extend_set h A == h ` (A <*> UNIV)"
 
   project_set :: "['a*'b => 'c, 'c set] => 'a set"
     "project_set h C == {x. EX y. h(x,y) : C}"
@@ -34,16 +34,16 @@
 
   extend :: "['a*'b => 'c, 'a program] => 'c program"
     "extend h F == mk_program (extend_set h (Init F),
-			       extend_act h `` Acts F,
-			       project_act h -`` AllowedActs F)"
+			       extend_act h ` Acts F,
+			       project_act h -` AllowedActs F)"
 
   (*Argument C allows weak safety laws to be projected*)
   project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
     "project h C F ==
        mk_program (project_set h (Init F),
-		   project_act h `` Restrict C `` Acts F,
+		   project_act h ` Restrict C ` Acts F,
 		   {act. Restrict (project_set h C) act :
-		         project_act h `` Restrict C `` AllowedActs F})"
+		         project_act h ` Restrict C ` AllowedActs F})"
 
 locale Extend =
   fixes 
--- a/src/HOL/UNITY/FP.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/FP.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -49,11 +49,11 @@
 qed "FP_weakest";
 
 Goalw [FP_def, stable_def, constrains_def]
-    "-(FP F) = (UN act: Acts F. -{s. act```{s} <= {s}})";
+    "-(FP F) = (UN act: Acts F. -{s. act``{s} <= {s}})";
 by (Blast_tac 1);
 qed "Compl_FP";
 
-Goal "A - (FP F) = (UN act: Acts F. A - {s. act```{s} <= {s}})";
+Goal "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})";
 by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1);
 qed "Diff_FP";
 
--- a/src/HOL/UNITY/Lift_prog.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -214,14 +214,14 @@
 (** guarantees **)
 
 Goalw [lift_def]
-     "(lift i F : (lift i `` X) guarantees (lift i `` Y)) = \
+     "(lift i F : (lift i ` X) guarantees (lift i ` Y)) = \
 \     (F : X guarantees Y)";
 by (stac (bij_lift_map RS rename_rename_guarantees_eq RS sym) 1);
 by (asm_simp_tac (simpset() addsimps [o_def]) 1);
 qed "lift_lift_guarantees_eq";
 
 Goal "(lift i F : X guarantees Y) = \
-\     (F : (rename (drop_map i) `` X) guarantees (rename (drop_map i) `` Y))";
+\     (F : (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))";
 by (asm_simp_tac 
     (simpset() addsimps [bij_lift_map RS rename_guarantees_eq_rename_inv,
 			 lift_def]) 1);
@@ -255,11 +255,11 @@
 
 (*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
 
-Goal "(f o fst) -`` A = (f-``A) <*> UNIV";
+Goal "(f o fst) -` A = (f-`A) <*> UNIV";
 by Auto_tac;
 qed "vimage_o_fst_eq";
 
-Goal "(sub i -``A) <*> UNIV = lift_set i (A <*> UNIV)";
+Goal "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)";
 by Auto_tac;
 qed "vimage_sub_eq_lift_set";
 
@@ -356,7 +356,7 @@
 qed "lift_transient_eq_disj";
 
 (*USELESS??*)
-Goal "lift_map i `` (A <*> UNIV) = \
+Goal "lift_map i ` (A <*> UNIV) = \
 \     (UN s:A. UN f. {insert_map i s f}) <*> UNIV";
 by (auto_tac (claset() addSIs [bexI, image_eqI],
               simpset() addsimps [lift_map_def]));
@@ -475,12 +475,12 @@
                          UNION_OK_lift_I]) 1); 
 qed "OK_lift_I";
 
-Goal "Allowed (lift i F) = lift i `` (Allowed F)";
+Goal "Allowed (lift i F) = lift i ` (Allowed F)";
 by (simp_tac (simpset() addsimps [lift_def, Allowed_rename]) 1); 
 qed "Allowed_lift"; 
 Addsimps [Allowed_lift];
 
-Goal "lift i `` preserves v = preserves (v o drop_map i)";
+Goal "lift i ` preserves v = preserves (v o drop_map i)";
 by (simp_tac (simpset() addsimps [rename_image_preserves, lift_def, 
                                   inv_lift_map_eq]) 1); 
 qed "lift_image_preserves";
--- a/src/HOL/UNITY/Lift_prog.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -25,7 +25,7 @@
     "drop_map i == %(g, uu). (g i, (delete_map i g, uu))"
 
   lift_set :: "[nat, ('b * ((nat=>'b) * 'c)) set] => ((nat=>'b) * 'c) set"
-    "lift_set i A == lift_map i `` A"
+    "lift_set i A == lift_map i ` A"
 
   lift :: "[nat, ('b * ((nat=>'b) * 'c)) program] => ((nat=>'b) * 'c) program"
     "lift i == rename (lift_map i)"
--- a/src/HOL/UNITY/PPROD.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/PPROD.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -127,7 +127,7 @@
 by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
 qed "guarantees_PLam_I";
 
-Goal "Allowed (PLam I F) = (INT i:I. lift i `` Allowed(F i))";
+Goal "Allowed (PLam I F) = (INT i:I. lift i ` Allowed(F i))";
 by (simp_tac (simpset() addsimps [PLam_def]) 1); 
 qed "Allowed_PLam";
 Addsimps [Allowed_PLam];
--- a/src/HOL/UNITY/PriorityAux.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/PriorityAux.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -20,14 +20,14 @@
 (* The equalities (above i r = {}) = (A i r = {}) 
    and (reach i r = {}) = (R i r) rely on the following theorem  *)
 
-Goal "((r^+)```{i} = {}) = (r```{i} = {})";
+Goal "((r^+)``{i} = {}) = (r``{i} = {})";
 by Auto_tac;
 by (etac trancl_induct 1);
 by Auto_tac;
 qed "image0_trancl_iff_image0_r";
 
 (* Another form usefull in some situation *)
-Goal "(r```{i}={}) = (ALL x. ((i,x):r^+) = False)";
+Goal "(r``{i}={}) = (ALL x. ((i,x):r^+) = False)";
 by Auto_tac;
 by (dtac (image0_trancl_iff_image0_r RS ssubst) 1);
 by Auto_tac;
@@ -76,7 +76,7 @@
 
 (* Lemma 2 *)
 Goal 
-"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)```{z}={})";
+"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)``{z}={})";
 by Auto_tac;
 by (forw_inst_tac [("r", "r")] trancl_into_trancl2 1);
 by Auto_tac;
@@ -86,7 +86,7 @@
  "acyclic r ==> A i r~={}-->(EX j:above i r. A j r = {})";
 by (full_simp_tac (simpset() 
             addsimps [acyclic_eq_wf, wf_eq_minimal]) 1);
-by (dres_inst_tac [("x", "((r^-1)^+)```{i}")] spec 1);
+by (dres_inst_tac [("x", "((r^-1)^+)``{i}")] spec 1);
 by Auto_tac;
 by (rotate_tac ~1 1);
 by (asm_full_simp_tac (simpset() 
--- a/src/HOL/UNITY/PriorityAux.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/PriorityAux.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -18,20 +18,20 @@
 
   (* Neighbors of a vertex i *)
   neighbors :: "[vertex, (vertex*vertex)set]=>vertex set"
- "neighbors i r == ((r Un r^-1)```{i}) - {i}"
+ "neighbors i r == ((r Un r^-1)``{i}) - {i}"
 
   R :: "[vertex, (vertex*vertex)set]=>vertex set"
-  "R i r == r```{i}"
+  "R i r == r``{i}"
 
   A :: "[vertex, (vertex*vertex)set]=>vertex set"
-  "A i r == (r^-1)```{i}"
+  "A i r == (r^-1)``{i}"
 
   (* reachable and above vertices: the original notation was R* and A* *)  
   reach :: "[vertex, (vertex*vertex)set]=> vertex set"
-  "reach i r == (r^+)```{i}"
+  "reach i r == (r^+)``{i}"
 
   above :: "[vertex, (vertex*vertex)set]=> vertex set"
-  "above i r == ((r^-1)^+)```{i}"  
+  "above i r == ((r^-1)^+)``{i}"  
 
   reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set"
   "reverse i r == (r - {(x,y). x=i | y=i} Int r) Un ({(x,y). x=i|y=i} Int r)^-1"
--- a/src/HOL/UNITY/Project.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Project.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -384,7 +384,7 @@
      "[| G : transient (C Int extend_set h A);  G : stable C |]  \
 \     ==> project h C G : transient (project_set h C Int A)";
 by (auto_tac (claset(), simpset() addsimps [Domain_project_act]));
-by (subgoal_tac "act ``` (C Int extend_set h A) <= - extend_set h A" 1);
+by (subgoal_tac "act `` (C Int extend_set h A) <= - extend_set h A" 1);
 by (asm_full_simp_tac 
     (simpset() addsimps [stable_def, constrains_def]) 2);
 by (Blast_tac 2);
@@ -502,8 +502,8 @@
 
 
 Goalw [project_set_def, extend_set_def, project_act_def]
-     "act ``` (C Int extend_set h A) <= B \
-\     ==> project_act h (Restrict C act) ``` (project_set h C Int A) \
+     "act `` (C Int extend_set h A) <= B \
+\     ==> project_act h (Restrict C act) `` (project_set h C Int A) \
 \         <= project_set h B";
 by (Blast_tac 1);
 qed "act_subset_imp_project_act_subset";
@@ -512,9 +512,9 @@
   property upwards.  The hard part would be to 
   show that G's action has a big enough domain.*)
 Goal "[| act: Acts G;       \
-\        (project_act h (Restrict C act))``` \
+\        (project_act h (Restrict C act))`` \
 \             (project_set h C Int A - B) <= -(project_set h C Int A - B) |] \
-\     ==> act```(C Int extend_set h A - extend_set h B) \
+\     ==> act``(C Int extend_set h A - extend_set h B) \
 \           <= -(C Int extend_set h A - extend_set h B)"; 
 by (auto_tac (claset(), 
      simpset() addsimps [project_set_def, extend_set_def, project_act_def]));  
@@ -535,8 +535,8 @@
 				  extend_set_Diff_distrib RS sym]));
 by (dtac act_subset_imp_project_act_subset 1);
 by (subgoal_tac
-    "project_act h (Restrict C act) ``` (project_set h C Int (A - B)) = {}" 1);
-by (REPEAT (thin_tac "?r```?A <= ?B" 1));
+    "project_act h (Restrict C act) `` (project_set h C Int (A - B)) = {}" 1);
+by (REPEAT (thin_tac "?r``?A <= ?B" 1));
 by (rewrite_goals_tac [project_set_def, extend_set_def, project_act_def]);
 by (Blast_tac 2);
 by (rtac ccontr 1);
--- a/src/HOL/UNITY/Reach.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Reach.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -108,7 +108,7 @@
 	      simpset() addsimps [fun_upd_idem]));
 qed "metric_le";
 
-Goal "Rprg : ((metric-``{m}) - fixedpoint) LeadsTo (metric-``(lessThan m))";
+Goal "Rprg : ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))";
 by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
 by (rtac LeadsTo_UN 1);
 by Auto_tac;
@@ -120,7 +120,7 @@
 	      simpset()));
 qed "LeadsTo_Diff_fixedpoint";
 
-Goal "Rprg : (metric-``{m}) LeadsTo (metric-``(lessThan m) Un fixedpoint)";
+Goal "Rprg : (metric-`{m}) LeadsTo (metric-`(lessThan m) Un fixedpoint)";
 by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R,
 	   subset_imp_LeadsTo] MRS LeadsTo_Diff) 1);
 by Auto_tac;
--- a/src/HOL/UNITY/Rename.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Rename.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -26,18 +26,18 @@
 by (etac surj_f_inv_f 1);
 qed "fst_o_inv_eq_inv";
 
-Goal "bij h ==> z : h``A = (inv h z : A)";
+Goal "bij h ==> z : h`A = (inv h z : A)";
 by (auto_tac (claset() addSIs [image_eqI],
 	      simpset() addsimps [bij_is_inj, bij_is_surj RS surj_f_inv_f]));
 qed "mem_rename_set_iff";
 
-Goal "extend_set (%(x,u). h x) A = h``A";
+Goal "extend_set (%(x,u). h x) A = h`A";
 by (auto_tac (claset() addSIs [image_eqI],
 	      simpset() addsimps [extend_set_def]));
 qed "extend_set_eq_image";
 Addsimps [extend_set_eq_image];
 
-Goalw [rename_def] "Init (rename h F) = h``(Init F)";
+Goalw [rename_def] "Init (rename h F) = h`(Init F)";
 by (Simp_tac 1);
 qed "Init_rename";
 
@@ -145,7 +145,7 @@
 by (asm_simp_tac (simpset() addsimps [export extend_inverse]) 1); 
 qed "inv_project_eq";
 
-Goal "bij h ==> Allowed (rename h F) = rename h `` Allowed F";
+Goal "bij h ==> Allowed (rename h F) = rename h ` Allowed F";
 by (asm_simp_tac (simpset() addsimps [rename_def, export Allowed_extend]) 1);
 by (stac bij_vimage_eq_inv_image 1); 
 by (rtac bij_project 1); 
@@ -209,17 +209,17 @@
 (*** Strong Safety: co, stable ***)
 
 Goalw [rename_def]
-     "bij h ==> (rename h F : (h``A) co (h``B)) = (F : A co B)";
+     "bij h ==> (rename h F : (h`A) co (h`B)) = (F : A co B)";
 by (REPEAT (stac (extend_set_eq_image RS sym) 1));
 by (etac (good_map_bij RS export extend_constrains) 1);
 qed "rename_constrains";
 
 Goalw [stable_def]
-     "bij h ==> (rename h F : stable (h``A)) = (F : stable A)";
+     "bij h ==> (rename h F : stable (h`A)) = (F : stable A)";
 by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1);
 qed "rename_stable";
 
-Goal "bij h ==> (rename h F : invariant (h``A)) = (F : invariant A)";
+Goal "bij h ==> (rename h F : invariant (h`A)) = (F : invariant A)";
 by (asm_simp_tac (simpset() addsimps [invariant_def, rename_stable,
 				      bij_is_inj RS inj_image_subset_iff]) 1);
 qed "rename_invariant";
@@ -234,22 +234,22 @@
 (*** Weak Safety: Co, Stable ***)
 
 Goalw [rename_def]
-     "bij h ==> reachable (rename h F) = h `` (reachable F)";
+     "bij h ==> reachable (rename h F) = h ` (reachable F)";
 by (asm_simp_tac (simpset() addsimps [export reachable_extend_eq]) 1);
 qed "reachable_rename_eq";
 
-Goal "bij h ==> (rename h F : (h``A) Co (h``B)) = (F : A Co B)";
+Goal "bij h ==> (rename h F : (h`A) Co (h`B)) = (F : A Co B)";
 by (asm_simp_tac
     (simpset() addsimps [Constrains_def, reachable_rename_eq, 
 			 rename_constrains, bij_is_inj, image_Int RS sym]) 1);
 qed "rename_Constrains";
 
 Goalw [Stable_def]
-     "bij h ==> (rename h F : Stable (h``A)) = (F : Stable A)";
+     "bij h ==> (rename h F : Stable (h`A)) = (F : Stable A)";
 by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1);
 qed "rename_Stable";
 
-Goal "bij h ==> (rename h F : Always (h``A)) = (F : Always A)";
+Goal "bij h ==> (rename h F : Always (h`A)) = (F : Always A)";
 by (asm_simp_tac (simpset() addsimps [Always_def, rename_Stable,
 				      bij_is_inj RS inj_image_subset_iff]) 1);
 qed "rename_Always";
@@ -264,32 +264,32 @@
 (*** Progress: transient, ensures ***)
 
 Goalw [rename_def]
-     "bij h ==> (rename h F : transient (h``A)) = (F : transient A)";
+     "bij h ==> (rename h F : transient (h`A)) = (F : transient A)";
 by (stac (extend_set_eq_image RS sym) 1);
 by (etac (good_map_bij RS export extend_transient) 1);
 qed "rename_transient";
 
 Goalw [rename_def]
-     "bij h ==> (rename h F : (h``A) ensures (h``B)) = (F : A ensures B)";
+     "bij h ==> (rename h F : (h`A) ensures (h`B)) = (F : A ensures B)";
 by (REPEAT (stac (extend_set_eq_image RS sym) 1));
 by (etac (good_map_bij RS export extend_ensures) 1);
 qed "rename_ensures";
 
 Goalw [rename_def]
-     "bij h ==> (rename h F : (h``A) leadsTo (h``B)) = (F : A leadsTo B)";
+     "bij h ==> (rename h F : (h`A) leadsTo (h`B)) = (F : A leadsTo B)";
 by (REPEAT (stac (extend_set_eq_image RS sym) 1));
 by (etac (good_map_bij RS export extend_leadsTo) 1);
 qed "rename_leadsTo";
 
 Goalw [rename_def]
-     "bij h ==> (rename h F : (h``A) LeadsTo (h``B)) = (F : A LeadsTo B)";
+     "bij h ==> (rename h F : (h`A) LeadsTo (h`B)) = (F : A LeadsTo B)";
 by (REPEAT (stac (extend_set_eq_image RS sym) 1));
 by (etac (good_map_bij RS export extend_LeadsTo) 1);
 qed "rename_LeadsTo";
 
 Goalw [rename_def]
-     "bij h ==> (rename h F : (rename h `` X) guarantees \
-\                             (rename h `` Y)) = \
+     "bij h ==> (rename h F : (rename h ` X) guarantees \
+\                             (rename h ` Y)) = \
 \               (F : X guarantees Y)";
 by (stac (good_map_bij RS export extend_guarantees_eq RS sym) 1);
 by (assume_tac 1);
@@ -297,8 +297,8 @@
 qed "rename_rename_guarantees_eq";
 
 Goal "bij h ==> (rename h F : X guarantees Y) = \
-\               (F : (rename (inv h) `` X) guarantees \
-\                    (rename (inv h) `` Y))";
+\               (F : (rename (inv h) ` X) guarantees \
+\                    (rename (inv h) ` Y))";
 by (stac (rename_rename_guarantees_eq RS sym) 1);
 by (assume_tac 1);
 by (asm_simp_tac
@@ -336,47 +336,47 @@
 	 (auto_tac (claset() addSIs [surj_rename RS surj_f_inv_f RS sym],
 	      simpset() addsimps ths))];
 
-Goal "bij h ==> rename h `` (A co B) = (h `` A) co (h``B)";
+Goal "bij h ==> rename h ` (A co B) = (h ` A) co (h`B)";
 by (rename_image_tac [rename_constrains]);
 qed "rename_image_constrains";
 
-Goal "bij h ==> rename h `` stable A = stable (h `` A)";
+Goal "bij h ==> rename h ` stable A = stable (h ` A)";
 by (rename_image_tac [rename_stable]);
 qed "rename_image_stable";
 
-Goal "bij h ==> rename h `` increasing func = increasing (func o inv h)";
+Goal "bij h ==> rename h ` increasing func = increasing (func o inv h)";
 by (rename_image_tac [rename_increasing, o_def, bij_is_inj]);
 qed "rename_image_increasing";
 
-Goal "bij h ==> rename h `` invariant A = invariant (h `` A)";
+Goal "bij h ==> rename h ` invariant A = invariant (h ` A)";
 by (rename_image_tac [rename_invariant]);
 qed "rename_image_invariant";
 
-Goal "bij h ==> rename h `` (A Co B) = (h `` A) Co (h``B)";
+Goal "bij h ==> rename h ` (A Co B) = (h ` A) Co (h`B)";
 by (rename_image_tac [rename_Constrains]);
 qed "rename_image_Constrains";
 
-Goal "bij h ==> rename h `` preserves v = preserves (v o inv h)";
+Goal "bij h ==> rename h ` preserves v = preserves (v o inv h)";
 by (asm_simp_tac (simpset() addsimps [o_def, rename_image_stable,
                     preserves_def, bij_image_INT, bij_image_Collect_eq]) 1); 
 qed "rename_image_preserves";
 
-Goal "bij h ==> rename h `` Stable A = Stable (h `` A)";
+Goal "bij h ==> rename h ` Stable A = Stable (h ` A)";
 by (rename_image_tac [rename_Stable]);
 qed "rename_image_Stable";
 
-Goal "bij h ==> rename h `` Increasing func = Increasing (func o inv h)";
+Goal "bij h ==> rename h ` Increasing func = Increasing (func o inv h)";
 by (rename_image_tac [rename_Increasing, o_def, bij_is_inj]);
 qed "rename_image_Increasing";
 
-Goal "bij h ==> rename h `` Always A = Always (h `` A)";
+Goal "bij h ==> rename h ` Always A = Always (h ` A)";
 by (rename_image_tac [rename_Always]);
 qed "rename_image_Always";
 
-Goal "bij h ==> rename h `` (A leadsTo B) = (h `` A) leadsTo (h``B)";
+Goal "bij h ==> rename h ` (A leadsTo B) = (h ` A) leadsTo (h`B)";
 by (rename_image_tac [rename_leadsTo]);
 qed "rename_image_leadsTo";
 
-Goal "bij h ==> rename h `` (A LeadsTo B) = (h `` A) LeadsTo (h``B)";
+Goal "bij h ==> rename h ` (A LeadsTo B) = (h ` A) LeadsTo (h`B)";
 by (rename_image_tac [rename_LeadsTo]);
 qed "rename_image_LeadsTo";
--- a/src/HOL/UNITY/SubstAx.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/SubstAx.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -313,8 +313,8 @@
 
 (** Meta or object quantifier ????? **)
 Goal "[| wf r;     \
-\        ALL m. F : (A Int f-``{m}) LeadsTo                     \
-\                           ((A Int f-``(r^-1 ``` {m})) Un B) |] \
+\        ALL m. F : (A Int f-`{m}) LeadsTo                     \
+\                           ((A Int f-`(r^-1 `` {m})) Un B) |] \
 \     ==> F : A LeadsTo B";
 by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1);
 by (etac leadsTo_wf_induct 1);
@@ -323,9 +323,9 @@
 
 
 Goal "[| wf r;     \
-\        ALL m:I. F : (A Int f-``{m}) LeadsTo                   \
-\                             ((A Int f-``(r^-1 ``` {m})) Un B) |] \
-\     ==> F : A LeadsTo ((A - (f-``I)) Un B)";
+\        ALL m:I. F : (A Int f-`{m}) LeadsTo                   \
+\                             ((A Int f-`(r^-1 `` {m})) Un B) |] \
+\     ==> F : A LeadsTo ((A - (f-`I)) Un B)";
 by (etac LeadsTo_wf_induct 1);
 by Safe_tac;
 by (case_tac "m:I" 1);
@@ -335,7 +335,7 @@
 
 
 val prems = 
-Goal "(!!m::nat. F : (A Int f-``{m}) LeadsTo ((A Int f-``(lessThan m)) Un B)) \
+Goal "(!!m::nat. F : (A Int f-`{m}) LeadsTo ((A Int f-`(lessThan m)) Un B)) \
 \     ==> F : A LeadsTo B";
 by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
 by (auto_tac (claset() addIs prems, simpset()));
@@ -353,17 +353,17 @@
 by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff]));
 qed "integ_0_le_induct";
 
-Goal "!!l::nat. [| ALL m:(greaterThan l). F : (A Int f-``{m}) LeadsTo   \
-\                                        ((A Int f-``(lessThan m)) Un B) |] \
-\           ==> F : A LeadsTo ((A Int (f-``(atMost l))) Un B)";
+Goal "!!l::nat. [| ALL m:(greaterThan l). F : (A Int f-`{m}) LeadsTo   \
+\                                        ((A Int f-`(lessThan m)) Un B) |] \
+\           ==> F : A LeadsTo ((A Int (f-`(atMost l))) Un B)";
 by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
 by (rtac (wf_less_than RS Bounded_induct) 1);
 by (Asm_simp_tac 1);
 qed "LessThan_bounded_induct";
 
-Goal "!!l::nat. [| ALL m:(lessThan l). F : (A Int f-``{m}) LeadsTo   \
-\                              ((A Int f-``(greaterThan m)) Un B) |] \
-\     ==> F : A LeadsTo ((A Int (f-``(atLeast l))) Un B)";
+Goal "!!l::nat. [| ALL m:(lessThan l). F : (A Int f-`{m}) LeadsTo   \
+\                              ((A Int f-`(greaterThan m)) Un B) |] \
+\     ==> F : A LeadsTo ((A Int (f-`(atLeast l))) Un B)";
 by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
     (wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
 by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
--- a/src/HOL/UNITY/Token.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Token.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -74,8 +74,7 @@
 by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
 qed "TR7_aux";
 
-Goal "({s. token s < N} Int token -`` {m}) = \
-\     (if m<N then token -`` {m} else {})";
+Goal "({s. token s < N} Int token -` {m}) = (if m<N then token -` {m} else {})";
 by Auto_tac;
 val token_lemma = result();
 
--- a/src/HOL/UNITY/UNITY.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/UNITY.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -383,17 +383,17 @@
 qed "Un_Diff_Diff";
 Addsimps [Un_Diff_Diff];
 
-Goal "Union(B) Int A = Union((%C. C Int A)``B)";
+Goal "Union(B) Int A = Union((%C. C Int A)`B)";
 by (Blast_tac 1);
 qed "Int_Union_Union";
 
 (** Needed for WF reasoning in WFair.ML **)
 
-Goal "less_than ``` {k} = greaterThan k";
+Goal "less_than `` {k} = greaterThan k";
 by (Blast_tac 1);
 qed "Image_less_than";
 
-Goal "less_than^-1 ``` {k} = lessThan k";
+Goal "less_than^-1 `` {k} = lessThan k";
 by (Blast_tac 1);
 qed "Image_inverse_less_than";
 
--- a/src/HOL/UNITY/UNITY.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/UNITY.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -51,7 +51,7 @@
 
 
 defs
-  constrains_def "A co B == {F. ALL act: Acts F. act```A <= B}"
+  constrains_def "A co B == {F. ALL act: Acts F. act``A <= B}"
 
   unless_def     "A unless B == (A-B) co (A Un B)"
 
--- a/src/HOL/UNITY/WFair.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/WFair.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -27,14 +27,14 @@
 qed "transient_strengthen";
 
 Goalw [transient_def]
-    "[| act: Acts F;  A <= Domain act;  act```A <= -A |] ==> F : transient A";
+    "[| act: Acts F;  A <= Domain act;  act``A <= -A |] ==> F : transient A";
 by (Blast_tac 1);
 qed "transientI";
 
 val major::prems = 
 Goalw [transient_def]
     "[| F : transient A;  \
-\       !!act. [| act: Acts F;  A <= Domain act;  act```A <= -A |] ==> P |] \
+\       !!act. [| act: Acts F;  A <= Domain act;  act``A <= -A |] ==> P |] \
 \    ==> P";
 by (rtac (major RS CollectD RS bexE) 1);
 by (blast_tac (claset() addIs prems) 1);
@@ -361,11 +361,11 @@
 (** The most general rule: r is any wf relation; f is any variant function **)
 
 Goal "[| wf r;     \
-\        ALL m. F : (A Int f-``{m}) leadsTo                     \
-\                   ((A Int f-``(r^-1 ``` {m})) Un B) |] \
-\     ==> F : (A Int f-``{m}) leadsTo B";
+\        ALL m. F : (A Int f-`{m}) leadsTo                     \
+\                   ((A Int f-`(r^-1 `` {m})) Un B) |] \
+\     ==> F : (A Int f-`{m}) leadsTo B";
 by (eres_inst_tac [("a","m")] wf_induct 1);
-by (subgoal_tac "F : (A Int (f -`` (r^-1 ``` {x}))) leadsTo B" 1);
+by (subgoal_tac "F : (A Int (f -` (r^-1 `` {x}))) leadsTo B" 1);
 by (stac vimage_eq_UN 2);
 by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2);
 by (blast_tac (claset() addIs [leadsTo_UN]) 2);
@@ -375,8 +375,8 @@
 
 (** Meta or object quantifier ? **)
 Goal "[| wf r;     \
-\        ALL m. F : (A Int f-``{m}) leadsTo                     \
-\                   ((A Int f-``(r^-1 ``` {m})) Un B) |] \
+\        ALL m. F : (A Int f-`{m}) leadsTo                     \
+\                   ((A Int f-`(r^-1 `` {m})) Un B) |] \
 \     ==> F : A leadsTo B";
 by (res_inst_tac [("t", "A")] subst 1);
 by (rtac leadsTo_UN 2);
@@ -387,9 +387,9 @@
 
 
 Goal "[| wf r;     \
-\        ALL m:I. F : (A Int f-``{m}) leadsTo                   \
-\                     ((A Int f-``(r^-1 ``` {m})) Un B) |] \
-\     ==> F : A leadsTo ((A - (f-``I)) Un B)";
+\        ALL m:I. F : (A Int f-`{m}) leadsTo                   \
+\                     ((A Int f-`(r^-1 `` {m})) Un B) |] \
+\     ==> F : A leadsTo ((A - (f-`I)) Un B)";
 by (etac leadsTo_wf_induct 1);
 by Safe_tac;
 by (case_tac "m:I" 1);
@@ -398,9 +398,9 @@
 qed "bounded_induct";
 
 
-(*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
+(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*)
 val prems = 
-Goal "[| !!m::nat. F : (A Int f-``{m}) leadsTo ((A Int f-``{..m(}) Un B) |] \
+Goal "[| !!m::nat. F : (A Int f-`{m}) leadsTo ((A Int f-`{..m(}) Un B) |] \
 \     ==> F : A leadsTo B";
 by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
 by (Asm_simp_tac 1);
@@ -408,8 +408,8 @@
 qed "lessThan_induct";
 
 Goal "!!l::nat. [| ALL m:(greaterThan l).    \
-\           F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
-\     ==> F : A leadsTo ((A Int (f-``(atMost l))) Un B)";
+\           F : (A Int f-`{m}) leadsTo ((A Int f-`(lessThan m)) Un B) |] \
+\     ==> F : A leadsTo ((A Int (f-`(atMost l))) Un B)";
 by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, 
 			       Compl_greaterThan RS sym]) 1);
 by (rtac (wf_less_than RS bounded_induct) 1);
@@ -417,8 +417,8 @@
 qed "lessThan_bounded_induct";
 
 Goal "!!l::nat. [| ALL m:(lessThan l).    \
-\           F : (A Int f-``{m}) leadsTo ((A Int f-``(greaterThan m)) Un B) |] \
-\     ==> F : A leadsTo ((A Int (f-``(atLeast l))) Un B)";
+\           F : (A Int f-`{m}) leadsTo ((A Int f-`(greaterThan m)) Un B) |] \
+\     ==> F : A leadsTo ((A Int (f-`(atLeast l))) Un B)";
 by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
     (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
 by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
--- a/src/HOL/UNITY/WFair.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/WFair.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -15,7 +15,7 @@
   (*This definition specifies weak fairness.  The rest of the theory
     is generic to all forms of fairness.*)
   transient :: "'a set => 'a program set"
-    "transient A == {F. EX act: Acts F. A <= Domain act & act```A <= -A}"
+    "transient A == {F. EX act: Acts F. A <= Domain act & act``A <= -A}"
 
   ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
     "A ensures B == (A-B co A Un B) Int transient (A-B)"
--- a/src/HOL/ex/Multiquote.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/ex/Multiquote.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -13,7 +13,7 @@
 
 syntax
   "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
-  "_antiquote" :: "('a => 'b) => 'b"         ("`_" [1000] 1000)
+  "_antiquote" :: "('a => 'b) => 'b"         ("_" [1000] 1000)
 
 parse_translation {*
   let
@@ -35,14 +35,14 @@
 
 text {* basic examples *}
 term ".(a + b + c)."
-term ".(a + b + c + `x + `y + 1)."
-term ".(`(f w) + `x)."
-term ".(f `x `y z)."
+term ".(a + b + c + x + y + 1)."
+term ".((f w) + x)."
+term ".(f x y z)."
 
 text {* advanced examples *}
-term ".(.(` `x + `y).)."
-term ".(.(` `x + `y). o `f)."
-term ".(`(f o `g))."
-term ".(.( ` `(f o `g) ).)."
+term ".(.( x + y).)."
+term ".(.( x + y). o f)."
+term ".((f o g))."
+term ".(.(  (f o g) ).)."
 
 end
--- a/src/HOL/ex/PiSets.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/ex/PiSets.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -38,7 +38,7 @@
 
 
 
-Goal "PiBij A B `` (Pi A B) = Graph A B";
+Goal "PiBij A B ` (Pi A B) = Graph A B";
 by (rtac equalityI 1);
 by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1);
 by (rtac subsetI 1);
--- a/src/HOL/ex/Tarski.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/ex/Tarski.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -400,7 +400,7 @@
 by (simp_tac (simpset() addsimps PO_simp) 1);
 qed "CLF_E2";
 
-Goal "f : CLF ``` {cl} ==> f : CLF ``` {dual cl}";
+Goal "f : CLF `` {cl} ==> f : CLF `` {dual cl}";
 by (afs [CLF_def, CL_dualCL, monotone_dual] 1); 
 by (afs [dualA_iff] 1);
 qed "CLF_dual";
--- a/src/HOL/ex/Tarski.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/ex/Tarski.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -94,7 +94,7 @@
   "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
 
 translations
-  "S <<= cl" == "S : sublattice ``` {cl}"
+  "S <<= cl" == "S : sublattice `` {cl}"
 
 constdefs
   dual :: "'a potype => 'a potype"
@@ -121,7 +121,7 @@
   f :: "'a => 'a"
   P :: "'a set"
 assumes 
-  f_cl "f : CLF```{cl}"
+  f_cl "f : CLF``{cl}"
 defines
   P_def "P == fix f A"
 
--- a/src/HOL/ex/set.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/ex/set.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -25,12 +25,12 @@
 (** Examples for the Blast_tac paper **)
 
 (*Union-image, called Un_Union_image on equalities.ML*)
-Goal "(UN x:C. f(x) Un g(x)) = Union(f``C)  Un  Union(g``C)";
+Goal "(UN x:C. f(x) Un g(x)) = Union(f`C)  Un  Union(g`C)";
 by (Blast_tac 1);
 qed "";
 
 (*Inter-image, called Int_Inter_image on equalities.ML*)
-Goal "(INT x:C. f(x) Int g(x)) = Inter(f``C) Int Inter(g``C)";
+Goal "(INT x:C. f(x) Int g(x)) = Inter(f`C) Int Inter(g`C)";
 by (Blast_tac 1);
 qed "";
 
@@ -83,24 +83,24 @@
 
 (*** The Schroeder-Berstein Theorem ***)
 
-Goal "[| -(f``X) = g``(-X);  f(a)=g(b);  a:X |] ==> b:X";
+Goal "[| -(f`X) = g`(-X);  f(a)=g(b);  a:X |] ==> b:X";
 by (Blast_tac 1);
 qed "disj_lemma";
 
-Goal "-(f``X) = g``(-X) ==> surj(%z. if z:X then f(z) else g(z))";
+Goal "-(f`X) = g`(-X) ==> surj(%z. if z:X then f(z) else g(z))";
 by (asm_simp_tac (simpset() addsimps [surj_def]) 1);
 by (Blast_tac 1);
 qed "surj_if_then_else";
 
 Goalw [inj_on_def]
-     "[| inj_on f X;  inj_on g (-X);  -(f``X) = g``(-X); \
+     "[| inj_on f X;  inj_on g (-X);  -(f`X) = g`(-X); \
 \        h = (%z. if z:X then f(z) else g(z)) |]       \
 \     ==> inj(h) & surj(h)";
 by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1);
 by (blast_tac (claset() addDs [disj_lemma, sym]) 1);
 qed "bij_if_then_else";
 
-Goal "EX X. X = - (g``(- (f``X)))";
+Goal "EX X. X = - (g`(- (f`X)))";
 by (rtac exI 1);
 by (rtac lfp_unfold 1);
 by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));
--- a/src/HOLCF/Cfun1.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Cfun1.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -50,15 +50,15 @@
 (* lemmas about application of continuous functions                         *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "[| f=g; x=y |] ==> f`x = g`y";
+Goal "[| f=g; x=y |] ==> f$x = g$y";
 by (Asm_simp_tac 1);
 qed "cfun_cong";
 
-Goal "f=g ==> f`x = g`x";
+Goal "f=g ==> f$x = g$x";
 by (Asm_simp_tac 1);
 qed "cfun_fun_cong";
 
-Goal "x=y ==> f`x = f`y";
+Goal "x=y ==> f$x = f$y";
 by (Asm_simp_tac 1);
 qed "cfun_arg_cong";
 
@@ -77,7 +77,7 @@
 (* simplification of application                                            *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "cont f ==> (Abs_CFun f)`x = f x";
+Goal "cont f ==> (Abs_CFun f)$x = f x";
 by (etac (Abs_Cfun_inverse2 RS fun_cong) 1);
 qed "Cfunapp2";
 
@@ -85,7 +85,7 @@
 (* beta - equality for continuous functions                                 *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "cont(c1) ==> (LAM x .c1 x)`u = c1 u";
+Goal "cont(c1) ==> (LAM x .c1 x)$u = c1 u";
 by (rtac Cfunapp2 1);
 by (atac 1);
 qed "beta_cfun";
--- a/src/HOLCF/Cfun1.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Cfun1.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -17,7 +17,7 @@
 instance "->"  :: (cpo,cpo)sq_ord
 
 syntax
-	Rep_CFun  :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
+	Rep_CFun  :: "('a -> 'b)=>('a => 'b)" ("_$_" [999,1000] 999)
                                                 (* application      *)
         Abs_CFun  :: "('a => 'b)=>('a -> 'b)"     (binder "LAM " 10)
                                                 (* abstraction      *)
--- a/src/HOLCF/Cfun2.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Cfun2.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -63,10 +63,10 @@
 (* ------------------------------------------------------------------------ *)
 
 bind_thm ("cont_cfun_arg", (cont_Rep_CFun2 RS contE RS spec RS mp));
-(* chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
+(* chain(?x1) ==> range (%i. ?fo3$(?x1 i)) <<| ?fo3$(lub (range ?x1))    *)
  
 bind_thm ("contlub_cfun_arg", (contlub_Rep_CFun2 RS contlubE RS spec RS mp));
-(* chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
+(* chain(?x1) ==> ?fo4$(lub (range ?x1)) = lub (range (%i. ?fo4$(?x1 i))) *)
 
 
 (* ------------------------------------------------------------------------ *)
@@ -83,7 +83,7 @@
 (* monotonicity of application Rep_CFun in mixfix syntax [_]_                   *)
 (* ------------------------------------------------------------------------ *)
 
-Goal  "f1 << f2 ==> f1`x << f2`x";
+Goal  "f1 << f2 ==> f1$x << f2$x";
 by (res_inst_tac [("x","x")] spec 1);
 by (rtac (less_fun RS subst) 1);
 by (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1);
@@ -91,20 +91,20 @@
 
 
 bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp);
-(* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1                                      *)
+(* ?x2 << ?x1 ==> ?fo5$?x2 << ?fo5$?x1                                      *)
 
 (* ------------------------------------------------------------------------ *)
 (* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_             *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2";
+Goal "[|f1<<f2;x1<<x2|] ==> f1$x1 << f2$x2";
 by (rtac trans_less 1);
 by (etac monofun_cfun_arg 1);
 by (etac monofun_cfun_fun 1);
 qed "monofun_cfun";
 
 
-Goal "f`x = UU ==> f`UU = UU";
+Goal "f$x = UU ==> f$UU = UU";
 by (rtac (eq_UU_iff RS iffD2) 1);
 by (etac subst 1);
 by (rtac (minimal RS monofun_cfun_arg) 1);
@@ -116,13 +116,13 @@
 (* use MF2 lemmas from Cont.ML                                              *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "chain(Y) ==> chain(%i. f`(Y i))";
+Goal "chain(Y) ==> chain(%i. f$(Y i))";
 by (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1);
 qed "ch2ch_Rep_CFunR";
 
 
 bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L);
-(* chain(?F) ==> chain (%i. ?F i`?x)                                  *)
+(* chain(?F) ==> chain (%i. ?F i$?x)                                  *)
 
 
 (* ------------------------------------------------------------------------ *)
@@ -130,7 +130,7 @@
 (* use MF2 lemmas from Cont.ML                                              *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))";
+Goal "chain(F) ==> monofun(% x. lub(range(% j.(F j)$x)))";
 by (rtac lub_MF2_mono 1);
 by (rtac monofun_Rep_CFun1 1);
 by (rtac (monofun_Rep_CFun2 RS allI) 1);
@@ -143,8 +143,8 @@
 (* ------------------------------------------------------------------------ *)
 
 Goal "[| chain(F); chain(Y) |] ==>\
-\               lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
-\               lub(range(%i. lub(range(%j. F(j)`(Y i)))))";
+\               lub(range(%j. lub(range(%i. F(j)$(Y i))))) =\
+\               lub(range(%i. lub(range(%j. F(j)$(Y i)))))";
 by (rtac ex_lubMF2 1);
 by (rtac monofun_Rep_CFun1 1);
 by (rtac (monofun_Rep_CFun2 RS allI) 1);
@@ -156,7 +156,7 @@
 (* the lub of a chain of cont. functions is continuous                      *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))";
+Goal "chain(F) ==> cont(% x. lub(range(% j. F(j)$x)))";
 by (rtac monocontlub2cont 1);
 by (etac lub_cfun_mono 1);
 by (rtac contlubI 1);
@@ -171,7 +171,7 @@
 (* type 'a -> 'b is chain complete                                          *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))";
+Goal "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)$x)))";
 by (rtac is_lubI 1);
 by (rtac ub_rangeI 1);
 by (stac less_cfun 1);
@@ -189,7 +189,7 @@
 
 bind_thm ("thelub_cfun", lub_cfun RS thelubI);
 (* 
-chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
+chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i$x)))
 *)
 
 Goal "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x";
@@ -202,7 +202,7 @@
 (* Extensionality in 'a -> 'b                                               *)
 (* ------------------------------------------------------------------------ *)
 
-val prems = Goal "(!!x. f`x = g`x) ==> f = g";
+val prems = Goal "(!!x. f$x = g$x) ==> f = g";
 by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
 by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
 by (res_inst_tac [("f","Abs_CFun")] arg_cong 1);
@@ -227,7 +227,7 @@
 (* Extenionality wrt. << in 'a -> 'b                                        *)
 (* ------------------------------------------------------------------------ *)
 
-val prems = Goal "(!!x. f`x << g`x) ==> f << g";
+val prems = Goal "(!!x. f$x << g$x) ==> f << g";
 by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
 by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
 by (rtac semi_monofun_Abs_CFun 1);
--- a/src/HOLCF/Cfun3.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Cfun3.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -47,7 +47,7 @@
 
 Goal 
 "chain(FY) ==>\
-\ lub(range FY)`x = lub(range (%i. FY(i)`x))";
+\ lub(range FY)$x = lub(range (%i. FY(i)$x))";
 by (rtac trans 1);
 by (etac (contlub_Rep_CFun1 RS contlubE RS spec RS mp RS fun_cong) 1);
 by (stac thelub_fun 1);
@@ -58,7 +58,7 @@
 
 Goal 
 "chain(FY) ==>\
-\ range(%i. FY(i)`x) <<| lub(range FY)`x";
+\ range(%i. FY(i)$x) <<| lub(range FY)$x";
 by (rtac thelubE 1);
 by (etac ch2ch_Rep_CFunL 1);
 by (etac (contlub_cfun_fun RS sym) 1);
@@ -71,7 +71,7 @@
 
 Goal 
 "[|chain(FY);chain(TY)|] ==>\
-\ (lub(range FY))`(lub(range TY)) = lub(range(%i. FY(i)`(TY i)))";
+\ (lub(range FY))$(lub(range TY)) = lub(range(%i. FY(i)$(TY i)))";
 by (rtac contlub_CF2 1);
 by (rtac cont_Rep_CFun1 1);
 by (rtac allI 1);
@@ -82,7 +82,7 @@
 
 Goal 
 "[|chain(FY);chain(TY)|] ==>\
-\ range(%i.(FY i)`(TY i)) <<| (lub (range FY))`(lub(range TY))";
+\ range(%i.(FY i)$(TY i)) <<| (lub (range FY))$(lub(range TY))";
 by (rtac thelubE 1);
 by (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1);
 by (rtac allI 1);
@@ -98,7 +98,7 @@
 (* cont2cont lemma for Rep_CFun                                               *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "[|cont(%x. ft x);cont(%x. tt x)|] ==> cont(%x. (ft x)`(tt x))";
+Goal "[|cont(%x. ft x);cont(%x. tt x)|] ==> cont(%x. (ft x)$(tt x))";
 by (best_tac (claset() addIs [cont2cont_app2, cont_const, cont_Rep_CFun1,
 	                      cont_Rep_CFun2]) 1);
 qed "cont2cont_Rep_CFun";
@@ -162,7 +162,7 @@
 (* function application _[_]  is strict in its first arguments              *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "(UU::'a::cpo->'b)`x = (UU::'b)";
+Goal "(UU::'a::cpo->'b)$x = (UU::'b)";
 by (stac inst_cfun_pcpo 1);
 by (stac beta_cfun 1);
 by (Simp_tac 1);
@@ -180,7 +180,7 @@
 qed "Istrictify1";
 
 Goalw [Istrictify_def]
-        "~x=UU ==> Istrictify(f)(x)=f`x";
+        "~x=UU ==> Istrictify(f)(x)=f$x";
 by (Asm_simp_tac 1);
 qed "Istrictify2";
 
@@ -251,7 +251,7 @@
 by (asm_simp_tac (simpset() addsimps [Istrictify1, chain_UU_I_inverse, chain_UU_I, Istrictify1]) 1);
 by (stac Istrictify2 1);
 by (atac 1);
-by (res_inst_tac [("s","lub(range(%i. f`(Y i)))")] trans 1);
+by (res_inst_tac [("s","lub(range(%i. f$(Y i)))")] trans 1);
 by (rtac contlub_cfun_arg 1);
 by (atac 1);
 by (rtac lub_equal2 1);
@@ -271,7 +271,7 @@
         (monofun_Istrictify2 RS monocontlub2cont)); 
 
 
-Goalw [strictify_def] "strictify`f`UU=UU";
+Goalw [strictify_def] "strictify$f$UU=UU";
 by (stac beta_cfun 1);
 by (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1, cont2cont_CF1L]) 1);
 by (stac beta_cfun 1);
@@ -279,7 +279,7 @@
 by (rtac Istrictify1 1);
 qed "strictify1";
 
-Goalw [strictify_def] "~x=UU ==> strictify`f`x=f`x";
+Goalw [strictify_def] "~x=UU ==> strictify$f$x=f$x";
 by (stac beta_cfun 1);
 by (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1, cont2cont_CF1L]) 1);
 by (stac beta_cfun 1);
@@ -307,7 +307,7 @@
 (* ------------------------------------------------------------------------ *)
 
 Goal "chain (Y::nat => 'a::cpo->'b::chfin) \
-\     ==> !s. ? n. lub(range(Y))`s = Y n`s";
+\     ==> !s. ? n. lub(range(Y))$s = Y n$s";
 by (rtac allI 1);
 by (stac contlub_cfun_fun 1);
 by (atac 1);
@@ -320,21 +320,21 @@
 (* ------------------------------------------------------------------------ *)
 
 Goal  
-"!!f g.[|!y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a) |] \
-\ ==> f`UU=UU & g`UU=UU";
+"!!f g.[|!y. f$(g$y)=(y::'b) ; !x. g$(f$x)=(x::'a) |] \
+\ ==> f$UU=UU & g$UU=UU";
 by (rtac conjI 1);
 by (rtac UU_I 1);
-by (res_inst_tac [("s","f`(g`(UU::'b))"),("t","UU::'b")] subst 1);
+by (res_inst_tac [("s","f$(g$(UU::'b))"),("t","UU::'b")] subst 1);
 by (etac spec 1);
 by (rtac (minimal RS monofun_cfun_arg) 1);
 by (rtac UU_I 1);
-by (res_inst_tac [("s","g`(f`(UU::'a))"),("t","UU::'a")] subst 1);
+by (res_inst_tac [("s","g$(f$(UU::'a))"),("t","UU::'a")] subst 1);
 by (etac spec 1);
 by (rtac (minimal RS monofun_cfun_arg) 1);
 qed "iso_strict";
 
 
-Goal "[|!x. rep`(ab`x)=x;!y. ab`(rep`y)=y; z~=UU|] ==> rep`z ~= UU";
+Goal "[|!x. rep$(ab$x)=x;!y. ab$(rep$y)=y; z~=UU|] ==> rep$z ~= UU";
 by (etac contrapos_nn 1);
 by (dres_inst_tac [("f","ab")] cfun_arg_cong 1);
 by (etac box_equals 1);
@@ -343,7 +343,7 @@
 by (atac 1);
 qed "isorep_defined";
 
-Goal "[|!x. rep`(ab`x) = x;!y. ab`(rep`y)=y ; z~=UU|] ==> ab`z ~= UU";
+Goal "[|!x. rep$(ab$x) = x;!y. ab$(rep$y)=y ; z~=UU|] ==> ab$z ~= UU";
 by (etac contrapos_nn 1);
 by (dres_inst_tac [("f","rep")] cfun_arg_cong 1);
 by (etac box_equals 1);
@@ -357,19 +357,19 @@
 (* ------------------------------------------------------------------------ *)
 
 Goal "!!f g.[|! Y::nat=>'a. chain Y --> (? n. max_in_chain n Y); \
-\ !y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a::chfin) |] \
+\ !y. f$(g$y)=(y::'b) ; !x. g$(f$x)=(x::'a::chfin) |] \
 \ ==> ! Y::nat=>'b. chain Y --> (? n. max_in_chain n Y)";
 by (rewtac max_in_chain_def);
 by (strip_tac 1);
 by (rtac exE 1);
-by (res_inst_tac [("P","chain(%i. g`(Y i))")] mp 1);
+by (res_inst_tac [("P","chain(%i. g$(Y i))")] mp 1);
 by (etac spec 1);
 by (etac ch2ch_Rep_CFunR 1);
 by (rtac exI 1);
 by (strip_tac 1);
-by (res_inst_tac [("s","f`(g`(Y x))"),("t","Y(x)")] subst 1);
+by (res_inst_tac [("s","f$(g$(Y x))"),("t","Y(x)")] subst 1);
 by (etac spec 1);
-by (res_inst_tac [("s","f`(g`(Y j))"),("t","Y(j)")] subst 1);
+by (res_inst_tac [("s","f$(g$(Y j))"),("t","Y(j)")] subst 1);
 by (etac spec 1);
 by (rtac cfun_arg_cong 1);
 by (rtac mp 1);
@@ -379,25 +379,25 @@
 
 
 Goal "!!f g.[|!x y::'a. x<<y --> x=UU | x=y; \
-\ !y. f`(g`y)=(y::'b); !x. g`(f`x)=(x::'a)|] ==> !x y::'b. x<<y --> x=UU | x=y";
+\ !y. f$(g$y)=(y::'b); !x. g$(f$x)=(x::'a)|] ==> !x y::'b. x<<y --> x=UU | x=y";
 by (strip_tac 1);
 by (rtac disjE 1);
-by (res_inst_tac [("P","g`x<<g`y")] mp 1);
+by (res_inst_tac [("P","g$x<<g$y")] mp 1);
 by (etac monofun_cfun_arg 2);
 by (dtac spec 1);
 by (etac spec 1);
 by (rtac disjI1 1);
 by (rtac trans 1);
-by (res_inst_tac [("s","f`(g`x)"),("t","x")] subst 1);
+by (res_inst_tac [("s","f$(g$x)"),("t","x")] subst 1);
 by (etac spec 1);
 by (etac cfun_arg_cong 1);
 by (rtac (iso_strict RS conjunct1) 1);
 by (atac 1);
 by (atac 1);
 by (rtac disjI2 1);
-by (res_inst_tac [("s","f`(g`x)"),("t","x")] subst 1);
+by (res_inst_tac [("s","f$(g$x)"),("t","x")] subst 1);
 by (etac spec 1);
-by (res_inst_tac [("s","f`(g`y)"),("t","y")] subst 1);
+by (res_inst_tac [("s","f$(g$y)"),("t","y")] subst 1);
 by (etac spec 1);
 by (etac cfun_arg_cong 1);
 qed "flat2flat";
@@ -406,19 +406,19 @@
 (* a result about functions with flat codomain                               *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "f`(x::'a)=(c::'b::flat) ==> f`(UU::'a)=(UU::'b) | (!z. f`(z::'a)=c)";
-by (case_tac "f`(x::'a)=(UU::'b)" 1);
+Goal "f$(x::'a)=(c::'b::flat) ==> f$(UU::'a)=(UU::'b) | (!z. f$(z::'a)=c)";
+by (case_tac "f$(x::'a)=(UU::'b)" 1);
 by (rtac disjI1 1);
 by (rtac UU_I 1);
-by (res_inst_tac [("s","f`(x)"),("t","UU::'b")] subst 1);
+by (res_inst_tac [("s","f$(x)"),("t","UU::'b")] subst 1);
 by (atac 1);
 by (rtac (minimal RS monofun_cfun_arg) 1);
-by (case_tac "f`(UU::'a)=(UU::'b)" 1);
+by (case_tac "f$(UU::'a)=(UU::'b)" 1);
 by (etac disjI1 1);
 by (rtac disjI2 1);
 by (rtac allI 1);
 by (hyp_subst_tac 1);
-by (res_inst_tac [("a","f`(UU::'a)")] (refl RS box_equals) 1);
+by (res_inst_tac [("a","f$(UU::'a)")] (refl RS box_equals) 1);
 by (res_inst_tac [("fo5","f")] ((minimal RS monofun_cfun_arg) RS (ax_flat RS spec RS spec RS mp) RS disjE) 1);
 by (contr_tac 1);
 by (atac 1);
@@ -433,13 +433,13 @@
 (* ------------------------------------------------------------------------ *)
 
 
-Goalw [ID_def] "ID`x=x";
+Goalw [ID_def] "ID$x=x";
 by (stac beta_cfun 1);
 by (rtac cont_id 1);
 by (rtac refl 1);
 qed "ID1";
 
-Goalw [oo_def] "(f oo g)=(LAM x. f`(g`x))";
+Goalw [oo_def] "(f oo g)=(LAM x. f$(g$x))";
 by (stac beta_cfun 1);
 by (Simp_tac 1);
 by (stac beta_cfun 1);
@@ -447,7 +447,7 @@
 by (rtac refl 1);
 qed "cfcomp1";
 
-Goal  "(f oo g)`x=f`(g`x)";
+Goal  "(f oo g)$x=f$(g$x)";
 by (stac cfcomp1 1);
 by (stac beta_cfun 1);
 by (Simp_tac 1);
@@ -481,7 +481,7 @@
 
 Goal "f oo (g oo h) = (f oo g) oo h";
 by (rtac ext_cfun 1);
-by (res_inst_tac [("s","f`(g`(h`x))")] trans  1);
+by (res_inst_tac [("s","f$(g$(h$x))")] trans  1);
 by (stac cfcomp2 1);
 by (stac cfcomp2 1);
 by (rtac refl 1);
--- a/src/HOLCF/Cfun3.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Cfun3.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -19,7 +19,7 @@
         strictify    :: "('a->'b)->'a->'b"
 defs
 
-Istrictify_def  "Istrictify f x == if x=UU then UU else f`x"    
+Istrictify_def  "Istrictify f x == if x=UU then UU else f$x"    
 strictify_def   "strictify == (LAM f x. Istrictify f x)"
 
 consts
@@ -28,11 +28,11 @@
 
 syntax  "@oo"   :: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
      
-translations    "f1 oo f2" == "cfcomp`f1`f2"
+translations    "f1 oo f2" == "cfcomp$f1$f2"
 
 defs
 
   ID_def        "ID ==(LAM x. x)"
-  oo_def        "cfcomp == (LAM f g x. f`(g`x))" 
+  oo_def        "cfcomp == (LAM f g x. f$(g$x))" 
 
 end
--- a/src/HOLCF/Cprod3.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Cprod3.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -125,7 +125,7 @@
 (* ------------------------------------------------------------------------ *)
 
 Goalw [cpair_def]
-        "(LAM x y.(x,y))`a`b = (a,b)";
+        "(LAM x y.(x,y))$a$b = (a,b)";
 by (stac beta_cfun 1);
 by (simp_tac (simpset() addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1);
 by (stac beta_cfun 1);
@@ -170,7 +170,7 @@
 qed "cprodE";
 
 Goalw [cfst_def,cpair_def] 
-        "cfst`<x,y>=x";
+        "cfst$<x,y>=x";
 by (stac beta_cfun_cprod 1);
 by (stac beta_cfun 1);
 by (rtac cont_fst 1);
@@ -178,22 +178,22 @@
 qed "cfst2";
 
 Goalw [csnd_def,cpair_def] 
-        "csnd`<x,y>=y";
+        "csnd$<x,y>=y";
 by (stac beta_cfun_cprod 1);
 by (stac beta_cfun 1);
 by (rtac cont_snd 1);
 by (Simp_tac  1);
 qed "csnd2";
 
-Goal "cfst`UU = UU";
+Goal "cfst$UU = UU";
 by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1);
 qed "cfst_strict";
 
-Goal "csnd`UU = UU";
+Goal "csnd$UU = UU";
 by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1);
 qed "csnd_strict";
 
-Goalw [cfst_def,csnd_def,cpair_def] "<cfst`p , csnd`p> = p";
+Goalw [cfst_def,csnd_def,cpair_def] "<cfst$p , csnd$p> = p";
 by (stac beta_cfun_cprod 1);
 by (stac beta_cfun 1);
 by (rtac cont_snd 1);
@@ -212,7 +212,7 @@
 
 Goalw [cfst_def,csnd_def,cpair_def]
 "[|chain(S)|] ==> range(S) <<| \
-\ <(lub(range(%i. cfst`(S i)))) , lub(range(%i. csnd`(S i)))>";
+\ <(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>";
 by (stac beta_cfun_cprod 1);
 by (stac (beta_cfun RS ext) 1);
 by (rtac cont_snd 1);
@@ -226,17 +226,17 @@
 (*
 chain ?S1 ==>
  lub (range ?S1) =
- <lub (range (%i. cfst`(?S1 i))), lub (range (%i. csnd`(?S1 i)))>" 
+ <lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>" 
 *)
 Goalw [csplit_def]
-        "csplit`f`<x,y> = f`x`y";
+        "csplit$f$<x,y> = f$x$y";
 by (stac beta_cfun 1);
 by (Simp_tac 1);
 by (simp_tac (simpset() addsimps [cfst2,csnd2]) 1);
 qed "csplit2";
 
 Goalw [csplit_def]
-  "csplit`cpair`z=z";
+  "csplit$cpair$z=z";
 by (stac beta_cfun 1);
 by (Simp_tac 1);
 by (simp_tac (simpset() addsimps [surjective_pairing_Cprod2]) 1);
--- a/src/HOLCF/Cprod3.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Cprod3.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -22,13 +22,13 @@
 
 translations
         "<x, y, z>"   == "<x, <y, z>>"
-        "<x, y>"      == "cpair`x`y"
+        "<x, y>"      == "cpair$x$y"
 
 defs
 cpair_def       "cpair  == (LAM x y.(x,y))"
 cfst_def        "cfst   == (LAM p. fst(p))"
 csnd_def        "csnd   == (LAM p. snd(p))"      
-csplit_def      "csplit == (LAM f p. f`(cfst`p)`(csnd`p))"
+csplit_def      "csplit == (LAM f p. f$(cfst$p)$(csnd$p))"
 
 
 
@@ -43,7 +43,7 @@
 
 constdefs
   CLet           :: "'a -> ('a -> 'b) -> 'b"
-  "CLet == LAM s f. f`s"
+  "CLet == LAM s f. f$s"
 
 
 (* syntax for Let *)
@@ -59,7 +59,7 @@
 
 translations
   "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
-  "Let x = a in e"          == "CLet`a`(LAM x. e)"
+  "Let x = a in e"          == "CLet$a$(LAM x. e)"
 
 
 (* syntax for LAM <x,y,z>.e *)
@@ -68,9 +68,9 @@
   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
 
 translations
-  "LAM <x,y,zs>.b"        == "csplit`(LAM x. LAM <y,zs>.b)"
-  "LAM <x,y>. LAM zs. b"  <= "csplit`(LAM x y zs. b)"
-  "LAM <x,y>.b"           == "csplit`(LAM x y. b)"
+  "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
+  "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
+  "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
 
 syntax (symbols)
   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
--- a/src/HOLCF/Fix.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Fix.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -10,7 +10,7 @@
 (* derive inductive properties of iterate from primitive recursion          *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "iterate (Suc n) F x = iterate n F (F`x)";
+Goal "iterate (Suc n) F x = iterate n F (F$x)";
 by (induct_tac "n" 1);
 by Auto_tac;  
 qed "iterate_Suc2";
@@ -20,7 +20,7 @@
 (* This property is essential since monotonicity of iterate makes no sense  *)
 (* ------------------------------------------------------------------------ *)
 
-Goalw [chain]  "x << F`x ==> chain (%i. iterate i F x)";
+Goalw [chain]  "x << F$x ==> chain (%i. iterate i F x)";
 by (strip_tac 1);
 by (induct_tac "i" 1);
 by Auto_tac;  
@@ -40,7 +40,7 @@
 (* ------------------------------------------------------------------------ *)
 
 
-Goalw [Ifix_def] "Ifix F =F`(Ifix F)";
+Goalw [Ifix_def] "Ifix F =F$(Ifix F)";
 by (stac contlub_cfun_arg 1);
 by (rtac chain_iterate 1);
 by (rtac antisym_less 1);
@@ -61,7 +61,7 @@
 qed "Ifix_eq";
 
 
-Goalw [Ifix_def] "F`x=x ==> Ifix(F) << x";
+Goalw [Ifix_def] "F$x=x ==> Ifix(F) << x";
 by (rtac is_lub_thelub 1);
 by (rtac chain_iterate 1);
 by (rtac ub_rangeI 1);
@@ -250,19 +250,19 @@
 (* propagate properties of Ifix to its continuous counterpart               *)
 (* ------------------------------------------------------------------------ *)
 
-Goalw [fix_def] "fix`F = F`(fix`F)";
+Goalw [fix_def] "fix$F = F$(fix$F)";
 by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1);
 by (rtac Ifix_eq 1);
 qed "fix_eq";
 
-Goalw [fix_def] "F`x = x ==> fix`F << x";
+Goalw [fix_def] "F$x = x ==> fix$F << x";
 by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1);
 by (etac Ifix_least 1);
 qed "fix_least";
 
 
 Goal
-"[| F`x = x; !z. F`z = z --> x << z |] ==> x = fix`F";
+"[| F$x = x; !z. F$z = z --> x << z |] ==> x = fix$F";
 by (rtac antisym_less 1);
 by (etac allE 1);
 by (etac mp 1);
@@ -271,22 +271,22 @@
 qed "fix_eqI";
 
 
-Goal "f == fix`F ==> f = F`f";
+Goal "f == fix$F ==> f = F$f";
 by (asm_simp_tac (simpset() addsimps [fix_eq RS sym]) 1);
 qed "fix_eq2";
 
-Goal "f == fix`F ==> f`x = F`f`x";
+Goal "f == fix$F ==> f$x = F$f$x";
 by (etac (fix_eq2 RS cfun_fun_cong) 1);
 qed "fix_eq3";
 
 fun fix_tac3 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i)); 
 
-Goal "f = fix`F ==> f = F`f";
+Goal "f = fix$F ==> f = F$f";
 by (hyp_subst_tac 1);
 by (rtac fix_eq 1);
 qed "fix_eq4";
 
-Goal "f = fix`F ==> f`x = F`f`x";
+Goal "f = fix$F ==> f$x = F$f$x";
 by (rtac trans 1);
 by (etac (fix_eq4 RS cfun_fun_cong) 1);
 by (rtac refl 1);
@@ -294,7 +294,7 @@
 
 fun fix_tac5 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i)); 
 
-(* proves the unfolding theorem for function equations f = fix`... *)
+(* proves the unfolding theorem for function equations f = fix$... *)
 fun fix_prover thy fixeq s = prove_goal thy s (fn prems => [
         (rtac trans 1),
         (rtac (fixeq RS fix_eq4) 1),
@@ -303,7 +303,7 @@
         (Simp_tac 1)
         ]);
 
-(* proves the unfolding theorem for function definitions f == fix`... *)
+(* proves the unfolding theorem for function definitions f == fix$... *)
 fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [
         (rtac trans 1),
         (rtac (fix_eq2) 1),
@@ -335,7 +335,7 @@
 (* direct connection between fix and iteration without Ifix                 *)
 (* ------------------------------------------------------------------------ *)
 
-Goalw [fix_def] "fix`F = lub(range(%i. iterate i F UU))";
+Goalw [fix_def] "fix$F = lub(range(%i. iterate i F UU))";
 by (fold_goals_tac [Ifix_def]);
 by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1);
 qed "fix_def2";
@@ -379,7 +379,7 @@
 (* ------------------------------------------------------------------------ *)
 
 val major::prems = Goal
-     "[| adm(P); P(UU); !!x. P(x) ==> P(F`x)|] ==> P(fix`F)";
+     "[| adm(P); P(UU); !!x. P(x) ==> P(F$x)|] ==> P(fix$F)";
 by (stac fix_def2 1);
 by (rtac (major RS admD) 1);
 by (rtac chain_iterate 1);
@@ -389,8 +389,8 @@
 by (asm_simp_tac (simpset() addsimps (iterate_Suc::prems)) 1);
 qed "fix_ind";
 
-val prems = Goal "[| f == fix`F; adm(P); \
-\       P(UU); !!x. P(x) ==> P(F`x)|] ==> P f";
+val prems = Goal "[| f == fix$F; adm(P); \
+\       P(UU); !!x. P(x) ==> P(F$x)|] ==> P f";
 by (cut_facts_tac prems 1);
 by (asm_simp_tac HOL_ss 1);
 by (etac fix_ind 1);
@@ -402,7 +402,7 @@
 (* computational induction for weak admissible formulae                     *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "[| admw(P); !n. P(iterate n F UU)|] ==> P(fix`F)";
+Goal "[| admw(P); !n. P(iterate n F UU)|] ==> P(fix$F)";
 by (stac fix_def2 1);
 by (rtac (admw_def2 RS iffD1 RS spec RS mp) 1);
 by (atac 1);
@@ -410,7 +410,7 @@
 by (etac spec 1);
 qed "wfix_ind";
 
-Goal "[| f == fix`F; admw(P); \
+Goal "[| f == fix$F; admw(P); \
 \       !n. P(iterate n F UU) |] ==> P f";
 by (asm_simp_tac HOL_ss 1);
 by (etac wfix_ind 1);
@@ -440,7 +440,7 @@
 (* some lemmata for functions with flat/chfin domain/range types	    *)
 (* ------------------------------------------------------------------------ *)
 
-val _ = goalw thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u`s))";
+val _ = goalw thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u$s))";
 by (strip_tac 1);
 by (dtac chfin_Rep_CFunR 1);
 by (eres_inst_tac [("x","s")] allE 1);
--- a/src/HOLCF/Fix.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Fix.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -20,7 +20,7 @@
 
 primrec
   iterate_0   "iterate 0 F x = x"
-  iterate_Suc "iterate (Suc n) F x  = F`(iterate n F x)"
+  iterate_Suc "iterate (Suc n) F x  = F$(iterate n F x)"
 
 defs
 
--- a/src/HOLCF/Lift.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Lift.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -81,25 +81,25 @@
 (* ---------------------------------------------------------- *)
 
 
-Goal "flift1 f`(Def x) = (f x)";
+Goal "flift1 f$(Def x) = (f x)";
 by (simp_tac (simpset() addsimps [flift1_def]) 1);
 qed"flift1_Def";
 
-Goal "flift2 f`(Def x) = Def (f x)";
+Goal "flift2 f$(Def x) = Def (f x)";
 by (simp_tac (simpset() addsimps [flift2_def]) 1);
 qed"flift2_Def";
 
-Goal "flift1 f`UU = UU";
+Goal "flift1 f$UU = UU";
 by (simp_tac (simpset() addsimps [flift1_def]) 1);
 qed"flift1_UU";
 
-Goal "flift2 f`UU = UU";
+Goal "flift2 f$UU = UU";
 by (simp_tac (simpset() addsimps [flift2_def]) 1);
 qed"flift2_UU";
 
 Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
 
-Goal "x~=UU ==> (flift2 f)`x~=UU";
+Goal "x~=UU ==> (flift2 f)$x~=UU";
 by (def_tac 1);
 qed"flift2_nUU";
 
--- a/src/HOLCF/Lift3.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Lift3.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -134,13 +134,13 @@
 
 (* Two specific lemmas for the combination of LCF and HOL terms *)
 
-Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
+Goal "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s)";
 by (rtac cont2cont_CF1L 1);
 by (REPEAT (resolve_tac cont_lemmas1 1));
 by Auto_tac;
 qed"cont_Rep_CFun_app";
 
-Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
+Goal "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s t)";
 by (rtac cont2cont_CF1L 1);
 by (etac cont_Rep_CFun_app 1);
 by (assume_tac 1);
--- a/src/HOLCF/Lift3.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Lift3.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -29,9 +29,9 @@
                    Undef => UU
                  | Def y => Def (f y)))"
  liftpair_def
-  "liftpair x  == (case (cfst`x) of 
+  "liftpair x  == (case (cfst$x) of 
                   Undef  => UU
-                | Def x1 => (case (csnd`x) of 
+                | Def x1 => (case (csnd$x) of 
                                Undef => UU
                              | Def x2 => Def (x1,x2)))"
 
--- a/src/HOLCF/Sprod3.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Sprod3.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -240,7 +240,7 @@
 (* ------------------------------------------------------------------------ *)
 
 Goalw [spair_def]
-        "(LAM x y. Ispair x y)`a`b = Ispair a b";
+        "(LAM x y. Ispair x y)$a$b = Ispair a b";
 by (stac beta_cfun 1);
 by (simp_tac (simpset() addsimps [cont_Ispair2, cont_Ispair1, cont2cont_CF1L]) 1);
 by (stac beta_cfun 1);
@@ -343,7 +343,7 @@
 
 
 Goalw [sfst_def] 
-        "p=UU==>sfst`p=UU";
+        "p=UU==>sfst$p=UU";
 by (stac beta_cfun 1);
 by (rtac cont_Isfst 1);
 by (rtac strict_Isfst 1);
@@ -352,7 +352,7 @@
 qed "strict_sfst";
 
 Goalw [sfst_def,spair_def] 
-        "sfst`(:UU,y:) = UU";
+        "sfst$(:UU,y:) = UU";
 by (stac beta_cfun_sprod 1);
 by (stac beta_cfun 1);
 by (rtac cont_Isfst 1);
@@ -360,7 +360,7 @@
 qed "strict_sfst1";
  
 Goalw [sfst_def,spair_def] 
-        "sfst`(:x,UU:) = UU";
+        "sfst$(:x,UU:) = UU";
 by (stac beta_cfun_sprod 1);
 by (stac beta_cfun 1);
 by (rtac cont_Isfst 1);
@@ -368,7 +368,7 @@
 qed "strict_sfst2";
 
 Goalw [ssnd_def] 
-        "p=UU==>ssnd`p=UU";
+        "p=UU==>ssnd$p=UU";
 by (stac beta_cfun 1);
 by (rtac cont_Issnd 1);
 by (rtac strict_Issnd 1);
@@ -377,7 +377,7 @@
 qed "strict_ssnd";
 
 Goalw [ssnd_def,spair_def] 
-        "ssnd`(:UU,y:) = UU";
+        "ssnd$(:UU,y:) = UU";
 by (stac beta_cfun_sprod 1);
 by (stac beta_cfun 1);
 by (rtac cont_Issnd 1);
@@ -385,7 +385,7 @@
 qed "strict_ssnd1";
 
 Goalw [ssnd_def,spair_def] 
-        "ssnd`(:x,UU:) = UU";
+        "ssnd$(:x,UU:) = UU";
 by (stac beta_cfun_sprod 1);
 by (stac beta_cfun 1);
 by (rtac cont_Issnd 1);
@@ -393,7 +393,7 @@
 qed "strict_ssnd2";
 
 Goalw [sfst_def,spair_def] 
-        "y~=UU ==>sfst`(:x,y:)=x";
+        "y~=UU ==>sfst$(:x,y:)=x";
 by (stac beta_cfun_sprod 1);
 by (stac beta_cfun 1);
 by (rtac cont_Isfst 1);
@@ -401,7 +401,7 @@
 qed "sfst2";
 
 Goalw [ssnd_def,spair_def] 
-        "x~=UU ==>ssnd`(:x,y:)=y";
+        "x~=UU ==>ssnd$(:x,y:)=y";
 by (stac beta_cfun_sprod 1);
 by (stac beta_cfun 1);
 by (rtac cont_Issnd 1);
@@ -410,7 +410,7 @@
 
 
 Goalw [sfst_def,ssnd_def,spair_def]
-        "p~=UU ==> sfst`p ~=UU & ssnd`p ~=UU";
+        "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU";
 by (stac beta_cfun 1);
 by (rtac cont_Issnd 1);
 by (stac beta_cfun 1);
@@ -420,7 +420,7 @@
 by (atac 1);
 qed "defined_sfstssnd";
  
-Goalw [sfst_def,ssnd_def,spair_def] "(:sfst`p , ssnd`p:) = p";
+Goalw [sfst_def,ssnd_def,spair_def] "(:sfst$p , ssnd$p:) = p";
 by (stac beta_cfun_sprod 1);
 by (stac beta_cfun 1);
 by (rtac cont_Issnd 1);
@@ -431,7 +431,7 @@
 
 Goalw [sfst_def,ssnd_def,spair_def]
 "chain(S) ==> range(S) <<| \
-\              (: lub(range(%i. sfst`(S i))), lub(range(%i. ssnd`(S i))) :)";
+\              (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)";
 by (stac beta_cfun_sprod 1);
 by (stac (beta_cfun RS ext) 1);
 by (rtac cont_Issnd 1);
@@ -445,11 +445,11 @@
 (*
  "chain ?S1 ==>
  lub (range ?S1) =
- (:lub (range (%i. sfst`(?S1 i))), lub (range (%i. ssnd`(?S1 i))):)" : thm
+ (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm
 *)
 
 Goalw [ssplit_def]
-        "ssplit`f`UU=UU";
+        "ssplit$f$UU=UU";
 by (stac beta_cfun 1);
 by (Simp_tac 1);
 by (stac strictify1 1);
@@ -457,7 +457,7 @@
 qed "ssplit1";
 
 Goalw [ssplit_def]
-        "[|x~=UU;y~=UU|] ==> ssplit`f`(:x,y:)= f`x`y";
+        "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y";
 by (stac beta_cfun 1);
 by (Simp_tac 1);
 by (stac strictify2 1);
@@ -475,7 +475,7 @@
 
 
 Goalw [ssplit_def]
-  "ssplit`spair`z=z";
+  "ssplit$spair$z=z";
 by (stac beta_cfun 1);
 by (Simp_tac 1);
 by (case_tac "z=UU" 1);
--- a/src/HOLCF/Sprod3.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Sprod3.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -21,12 +21,12 @@
 
 translations
         "(:x, y, z:)"   == "(:x, (:y, z:):)"
-        "(:x, y:)"      == "spair`x`y"
+        "(:x, y:)"      == "spair$x$y"
 
 defs
 spair_def       "spair  == (LAM x y. Ispair x y)"
 sfst_def        "sfst   == (LAM p. Isfst p)"
 ssnd_def        "ssnd   == (LAM p. Issnd p)"     
-ssplit_def      "ssplit == (LAM f. strictify`(LAM p. f`(sfst`p)`(ssnd`p)))"
+ssplit_def      "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
 
 end
--- a/src/HOLCF/Ssum0.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Ssum0.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -237,7 +237,7 @@
 
 
 Goalw [Iwhen_def]
-        "x~=UU ==> Iwhen f g (Isinl x) = f`x";
+        "x~=UU ==> Iwhen f g (Isinl x) = f$x";
 by (rtac some_equality 1);
 by (fast_tac HOL_cs  2);
 by (rtac conjI 1);
@@ -260,7 +260,7 @@
 qed "Iwhen2";
 
 Goalw [Iwhen_def]
-        "y~=UU ==> Iwhen f g (Isinr y) = g`y";
+        "y~=UU ==> Iwhen f g (Isinr y) = g$y";
 by (rtac some_equality 1);
 by (fast_tac HOL_cs  2);
 by (rtac conjI 1);
--- a/src/HOLCF/Ssum0.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Ssum0.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -31,7 +31,7 @@
 
   Iwhen_def     "Iwhen(f)(g)(s) == @z.
                                     (s=Isinl(UU) --> z=UU)
-                        &(!a. a~=UU & s=Isinl(a) --> z=f`a)  
-                        &(!b. b~=UU & s=Isinr(b) --> z=g`b)"  
+                        &(!a. a~=UU & s=Isinl(a) --> z=f$a)  
+                        &(!b. b~=UU & s=Isinr(b) --> z=g$b)"  
 
 end
--- a/src/HOLCF/Ssum3.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Ssum3.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -319,43 +319,43 @@
 (* continuous versions of lemmas for 'a ++ 'b                               *)
 (* ------------------------------------------------------------------------ *)
 
-Goalw [sinl_def] "sinl`UU =UU";
+Goalw [sinl_def] "sinl$UU =UU";
 by (simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1);
 by (rtac (inst_ssum_pcpo RS sym) 1);
 qed "strict_sinl";
 Addsimps [strict_sinl];
 
-Goalw [sinr_def] "sinr`UU=UU";
+Goalw [sinr_def] "sinr$UU=UU";
 by (simp_tac (Ssum0_ss addsimps [cont_Isinr]) 1);
 by (rtac (inst_ssum_pcpo RS sym) 1);
 qed "strict_sinr";
 Addsimps [strict_sinr];
 
 Goalw [sinl_def,sinr_def] 
-        "sinl`a=sinr`b ==> a=UU & b=UU";
+        "sinl$a=sinr$b ==> a=UU & b=UU";
 by (auto_tac (claset() addSDs [noteq_IsinlIsinr], simpset()));
 qed "noteq_sinlsinr";
 
 Goalw [sinl_def,sinr_def] 
-        "sinl`a1=sinl`a2==> a1=a2";
+        "sinl$a1=sinl$a2==> a1=a2";
 by Auto_tac;
 qed "inject_sinl";
 
 Goalw [sinl_def,sinr_def] 
-        "sinr`a1=sinr`a2==> a1=a2";
+        "sinr$a1=sinr$a2==> a1=a2";
 by Auto_tac;
 qed "inject_sinr";
 
 AddSDs [inject_sinl, inject_sinr];
 
-Goal "x~=UU ==> sinl`x ~= UU";
+Goal "x~=UU ==> sinl$x ~= UU";
 by (etac contrapos_nn 1);
 by (rtac inject_sinl 1);
 by Auto_tac;
 qed "defined_sinl";
 Addsimps [defined_sinl];
 
-Goal "x~=UU ==> sinr`x ~= UU";
+Goal "x~=UU ==> sinr$x ~= UU";
 by (etac contrapos_nn 1);
 by (rtac inject_sinr 1);
 by Auto_tac;
@@ -363,7 +363,7 @@
 Addsimps [defined_sinr];
 
 Goalw [sinl_def,sinr_def] 
-        "z=UU | (? a. z=sinl`a & a~=UU) | (? b. z=sinr`b & b~=UU)";
+        "z=UU | (? a. z=sinl$a & a~=UU) | (? b. z=sinr$b & b~=UU)";
 by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
 by (stac inst_ssum_pcpo 1);
 by (rtac Exh_Ssum 1);
@@ -372,8 +372,8 @@
 
 val [major,prem2,prem3] = Goalw [sinl_def,sinr_def] 
         "[|p=UU ==> Q ;\
-\       !!x.[|p=sinl`x; x~=UU |] ==> Q;\
-\       !!y.[|p=sinr`y; y~=UU |] ==> Q|] ==> Q";
+\       !!x.[|p=sinl$x; x~=UU |] ==> Q;\
+\       !!y.[|p=sinr$y; y~=UU |] ==> Q|] ==> Q";
 by (rtac (major RS IssumE) 1);
 by (stac inst_ssum_pcpo 1);
 by (atac 1);
@@ -387,8 +387,8 @@
 
 
 val [preml,premr] = Goalw [sinl_def,sinr_def] 
-      "[|!!x.[|p=sinl`x|] ==> Q;\
-\        !!y.[|p=sinr`y|] ==> Q|] ==> Q";
+      "[|!!x.[|p=sinl$x|] ==> Q;\
+\        !!y.[|p=sinr$y|] ==> Q|] ==> Q";
 by (rtac IssumE2 1);
 by (rtac preml 1);
 by (rtac premr 2);
@@ -399,7 +399,7 @@
                 cont_Iwhen3,cont2cont_CF1L]) 1)); 
 
 Goalw [sscase_def,sinl_def,sinr_def] 
-        "sscase`f`g`UU = UU";
+        "sscase$f$g$UU = UU";
 by (stac inst_ssum_pcpo 1);
 by (stac beta_cfun 1);
 by tac;
@@ -416,7 +416,7 @@
                 cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1));
 
 Goalw [sscase_def,sinl_def,sinr_def] 
-        "x~=UU==> sscase`f`g`(sinl`x) = f`x";
+        "x~=UU==> sscase$f$g$(sinl$x) = f$x";
 by (stac beta_cfun 1);
 by tac;
 by (stac beta_cfun 1);
@@ -430,7 +430,7 @@
 Addsimps [sscase2];
 
 Goalw [sscase_def,sinl_def,sinr_def] 
-        "x~=UU==> sscase`f`g`(sinr`x) = g`x";
+        "x~=UU==> sscase$f$g$(sinr$x) = g$x";
 by (stac beta_cfun 1);
 by tac;
 by (stac beta_cfun 1);
@@ -445,7 +445,7 @@
 
 
 Goalw [sinl_def,sinr_def] 
-        "(sinl`x << sinl`y) = (x << y)";
+        "(sinl$x << sinl$y) = (x << y)";
 by (stac beta_cfun 1);
 by tac;
 by (stac beta_cfun 1);
@@ -454,7 +454,7 @@
 qed "less_ssum4a";
 
 Goalw [sinl_def,sinr_def] 
-        "(sinr`x << sinr`y) = (x << y)";
+        "(sinr$x << sinr$y) = (x << y)";
 by (stac beta_cfun 1);
 by tac;
 by (stac beta_cfun 1);
@@ -463,7 +463,7 @@
 qed "less_ssum4b";
 
 Goalw [sinl_def,sinr_def] 
-        "(sinl`x << sinr`y) = (x = UU)";
+        "(sinl$x << sinr$y) = (x = UU)";
 by (stac beta_cfun 1);
 by tac;
 by (stac beta_cfun 1);
@@ -472,7 +472,7 @@
 qed "less_ssum4c";
 
 Goalw [sinl_def,sinr_def] 
-        "(sinr`x << sinl`y) = (x = UU)";
+        "(sinr$x << sinl$y) = (x = UU)";
 by (stac beta_cfun 1);
 by tac;
 by (stac beta_cfun 1);
@@ -481,15 +481,15 @@
 qed "less_ssum4d";
 
 Goalw [sinl_def,sinr_def] 
-        "chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)";
+        "chain(Y) ==> (!i.? x.(Y i)=sinl$x)|(!i.? y.(Y i)=sinr$y)";
 by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
 by (etac ssum_lemma4 1);
 qed "ssum_chainE";
 
 
 Goalw [sinl_def,sinr_def,sscase_def] 
-"[| chain(Y); !i.? x. Y(i) = sinl`x |] ==>\ 
-\   lub(range(Y)) = sinl`(lub(range(%i. sscase`(LAM x. x)`(LAM y. UU)`(Y i))))";
+"[| chain(Y); !i.? x. Y(i) = sinl$x |] ==>\ 
+\   lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i))))";
 by (stac beta_cfun 1);
 by tac;
 by (stac beta_cfun 1);
@@ -510,8 +510,8 @@
 qed "thelub_ssum2a";
 
 Goalw [sinl_def,sinr_def,sscase_def] 
-"[| chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ 
-\   lub(range(Y)) = sinr`(lub(range(%i. sscase`(LAM y. UU)`(LAM x. x)`(Y i))))";
+"[| chain(Y); !i.? x. Y(i) = sinr$x |] ==>\ 
+\   lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))";
 by (stac beta_cfun 1);
 by tac;
 by (stac beta_cfun 1);
@@ -532,22 +532,22 @@
 qed "thelub_ssum2b";
 
 Goalw [sinl_def,sinr_def] 
-        "[| chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x";
+        "[| chain(Y); lub(range(Y)) = sinl$x|] ==> !i.? x. Y(i)=sinl$x";
 by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1);
 by (etac ssum_lemma9 1);
 by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1);
 qed "thelub_ssum2a_rev";
 
 Goalw [sinl_def,sinr_def] 
-     "[| chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x";
+     "[| chain(Y); lub(range(Y)) = sinr$x|] ==> !i.? x. Y(i)=sinr$x";
 by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1);
 by (etac ssum_lemma10 1);
 by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1);
 qed "thelub_ssum2b_rev";
 
 Goal "chain(Y) ==>\ 
-\   lub(range(Y)) = sinl`(lub(range(%i. sscase`(LAM x. x)`(LAM y. UU)`(Y i))))\
-\ | lub(range(Y)) = sinr`(lub(range(%i. sscase`(LAM y. UU)`(LAM x. x)`(Y i))))";
+\   lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i))))\
+\ | lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))";
 by (rtac (ssum_chainE RS disjE) 1);
 by (atac 1);
 by (rtac disjI1 1);
@@ -558,7 +558,7 @@
 by (atac 1);
 qed "thelub_ssum3";
 
-Goal "sscase`sinl`sinr`z=z";
+Goal "sscase$sinl$sinr$z=z";
 by (res_inst_tac [("p","z")] ssumE 1);
 by Auto_tac;
 qed "sscase4";
--- a/src/HOLCF/Ssum3.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Ssum3.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -22,6 +22,6 @@
 sscase_def      "sscase   == (LAM f g s. Iwhen(f)(g)(s))"
 
 translations
-"case s of sinl`x => t1 | sinr`y => t2" == "sscase`(LAM x. t1)`(LAM y. t2)`s"
+"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s"
 
 end
--- a/src/HOLCF/Tr.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Tr.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -72,9 +72,9 @@
 			"(y orelse y) = y"]);
 
 bind_thms ("neg_thms", map prover [
-                        "neg`TT = FF",
-                        "neg`FF = TT",
-                        "neg`UU = UU"
+                        "neg$TT = FF",
+                        "neg$FF = TT",
+                        "neg$UU = UU"
                         ]);
 
 bind_thms ("ifte_thms", map prover [
--- a/src/HOLCF/Tr.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Tr.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -27,14 +27,14 @@
         "@orelse"       :: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
  
 translations 
-	     "x andalso y" == "trand`x`y"
-             "x orelse y"  == "tror`x`y"
-             "If b then e1 else e2 fi" == "Icifte`b`e1`e2"
+	     "x andalso y" == "trand$x$y"
+             "x orelse y"  == "tror$x$y"
+             "If b then e1 else e2 fi" == "Icifte$b$e1$e2"
 defs
   TT_def      "TT==Def True"
   FF_def      "FF==Def False"
   neg_def     "neg == flift2 Not"
-  ifte_def    "Icifte == (LAM b t e. flift1(%b. if b then t else e)`b)"
+  ifte_def    "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
   andalso_def "trand == (LAM x y. If x then y else FF fi)"
   orelse_def  "tror == (LAM x y. If x then TT else y fi)"
   If2_def     "If2 Q x y == If Q then x else y fi"
--- a/src/HOLCF/Up1.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Up1.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -64,7 +64,7 @@
 qed "Ifup1";
 
 Goalw [Ifup_def,Iup_def]
-        "Ifup(f)(Iup(x))=f`x";
+        "Ifup(f)(Iup(x))=f$x";
 by (stac Abs_Up_inverse2 1);
 by (stac sum_case_Inr 1);
 by (rtac refl 1);
--- a/src/HOLCF/Up1.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Up1.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -22,7 +22,7 @@
 
 defs
   Iup_def     "Iup x == Abs_Up(Inr(x))"
-  Ifup_def    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z"
+  Ifup_def    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f$z"
   less_up_def "(op <<) == (%x1 x2. case Rep_Up(x1) of                 
                Inl(y1) => True          
              | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
--- a/src/HOLCF/Up3.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Up3.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -133,23 +133,23 @@
 (* continuous versions of lemmas for ('a)u                                  *)
 (* ------------------------------------------------------------------------ *)
 
-Goalw [up_def] "z = UU | (EX x. z = up`x)";
+Goalw [up_def] "z = UU | (EX x. z = up$x)";
 by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
 by (stac inst_up_pcpo 1);
 by (rtac Exh_Up 1);
 qed "Exh_Up1";
 
-Goalw [up_def] "up`x=up`y ==> x=y";
+Goalw [up_def] "up$x=up$y ==> x=y";
 by (rtac inject_Iup 1);
 by Auto_tac;
 qed "inject_up";
 
-Goalw [up_def] " up`x ~= UU";
+Goalw [up_def] " up$x ~= UU";
 by Auto_tac;
 qed "defined_up";
 
 val prems = Goalw [up_def] 
-        "[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q";
+        "[| p=UU ==> Q; !!x. p=up$x==>Q|] ==>Q";
 by (rtac upE 1);
 by (resolve_tac prems 1);
 by (etac (inst_up_pcpo RS ssubst) 1);
@@ -160,7 +160,7 @@
 val tac = (simp_tac (simpset() addsimps [cont_Iup,cont_Ifup1,
                 cont_Ifup2,cont2cont_CF1L]) 1);
 
-Goalw [up_def,fup_def] "fup`f`UU=UU";
+Goalw [up_def,fup_def] "fup$f$UU=UU";
 by (stac inst_up_pcpo 1);
 by (stac beta_cfun 1);
 by tac;
@@ -169,7 +169,7 @@
 by (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1);
 qed "fup1";
 
-Goalw [up_def,fup_def] "fup`f`(up`x)=f`x";
+Goalw [up_def,fup_def] "fup$f$(up$x)=f$x";
 by (stac beta_cfun 1);
 by (rtac cont_Iup 1);
 by (stac beta_cfun 1);
@@ -179,20 +179,20 @@
 by (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1);
 qed "fup2";
 
-Goalw [up_def,fup_def] "~ up`x << UU";
+Goalw [up_def,fup_def] "~ up$x << UU";
 by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
 by (rtac less_up3b 1);
 qed "less_up4b";
 
 Goalw [up_def,fup_def]
-         "(up`x << up`y) = (x<<y)";
+         "(up$x << up$y) = (x<<y)";
 by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
 by (rtac less_up2c 1);
 qed "less_up4c";
 
 Goalw [up_def,fup_def] 
-"[| chain(Y); EX i x. Y(i) = up`x |] ==>\
-\      lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))";
+"[| chain(Y); EX i x. Y(i) = up$x |] ==>\
+\      lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))";
 by (stac beta_cfun 1);
 by tac;
 by (stac beta_cfun 1);
@@ -213,7 +213,7 @@
 
 
 Goalw [up_def,fup_def] 
-"[| chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU";
+"[| chain(Y); ! i x. Y(i) ~= up$x |] ==> lub(range(Y)) = UU";
 by (stac inst_up_pcpo 1);
 by (rtac thelub_up1b 1);
 by (atac 1);
@@ -224,7 +224,7 @@
 qed "thelub_up2b";
 
 
-Goal "(EX x. z = up`x) = (z~=UU)";
+Goal "(EX x. z = up$x) = (z~=UU)";
 by (rtac iffI 1);
 by (etac exE 1);
 by (hyp_subst_tac 1);
@@ -236,7 +236,7 @@
 qed "up_lemma2";
 
 
-Goal "[| chain(Y); lub(range(Y)) = up`x |] ==> EX i x. Y(i) = up`x";
+Goal "[| chain(Y); lub(range(Y)) = up$x |] ==> EX i x. Y(i) = up$x";
 by (rtac exE 1);
 by (rtac chain_UU_I_inverse2 1);
 by (rtac (up_lemma2 RS iffD1) 1);
@@ -246,14 +246,14 @@
 by (atac 1);
 qed "thelub_up2a_rev";
 
-Goal "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up`x";
+Goal "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up$x";
 by (blast_tac (claset() addSDs [chain_UU_I RS spec, 
                                 exI RS (up_lemma2 RS iffD1)]) 1);
 qed "thelub_up2b_rev";
 
 
 Goal "chain(Y) ==> lub(range(Y)) = UU | \
-\                  lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))";
+\                  lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))";
 by (rtac disjE 1);
 by (rtac disjI1 2);
 by (rtac thelub_up2b 2);
@@ -266,7 +266,7 @@
 by (fast_tac HOL_cs 1);
 qed "thelub_up3";
 
-Goal "fup`up`x=x";
+Goal "fup$up$x=x";
 by (res_inst_tac [("p","x")] upE1 1);
 by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1);
 by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1);
--- a/src/HOLCF/Up3.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Up3.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -19,7 +19,7 @@
        "fup == (LAM f p. Ifup(f)(p))"
 
 translations
-"case l of up`x => t1" == "fup`(LAM x. t1)`l"
+"case l of up$x => t1" == "fup$(LAM x. t1)$l"
 
 end