src/HOL/Hyperreal/NatStar.ML

           "a : A ==> hypnat_of_nat a : *sNat* A";
 by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],
          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";
 
 Goal "SNat <= *sNat* (UNIV:: nat set)";
 by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff,
                           NatStar_hypreal_of_real_image_subset]) 1);
 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]));
 by (fold_tac [hypnat_of_nat_def]);
 by (rtac imageI 1 THEN rtac ccontr 1);

 by (rtac lemma_hypnatrel_refl 1);
 by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2);
 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";
 
 Goalw [starsetNat_n_def,starsetNat_def] "*sNat* X = *sNatn* (%n. X)";
 by Auto_tac;

      "ALL n. (F n = f) ==> *fNat2n* F = *fNat2* f";
 by (Auto_tac);
 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);
 by (Auto_tac THEN Fuf_tac 1);
 qed "starfunNat";
 
 (* 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,
     [equiv_hypnatrel, starfunNat_congruent] MRS UN_equiv_class]) 1);
 qed "starfunNat2";

 
 (*----------------------------------------------------------
      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);
 qed "starfunNat_n";
 

 Goal "- (*fNatn* f) x = (*fNatn* (%i x. - (f i) x)) x";
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 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];
 
 Goal "((*fNat* f) = (*fNat* g)) = (f = g)";