src/HOL/Hyperreal/SEQ.ML

     simpset() addsimps [Compl_less_set]));
 qed "FreeUltrafilterNat_NSLIMSEQ";
 
 (* 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);
 qed "HNatInfinite_NSLIMSEQ";
 

 \     = {}";
 by Auto_tac;  
 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,
     hypreal_minus,hypreal_add,
     Infinitesimal_FreeUltrafilterNat_iff]));

       "X ----NS> L ==> X ----> L";
 by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
 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);
 by (blast_tac (claset() addIs [rename_numerals lemmaLIM3]) 1);
 qed "NSLIMSEQ_LIMSEQ";

 by (dtac choice 1);
 by (Blast_tac 1);
 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]);
 by (cut_inst_tac [("u","u")] FreeUltrafilterNat_nat_gt_real 1);
 by (dtac FreeUltrafilterNat_all 1);

 by (auto_tac (claset() addIs [finite_real_of_nat_less_real], 
               simpset() addsimps [real_of_nat_Suc, real_less_diff_eq RS sym]));
 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]);
 by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
 by (asm_full_simp_tac (simpset() addsimps 

    Equivalence between NS and standard definitions of Cauchy seqs
  ------------------------------------------------------------------*)
 (*-------------------------------
       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]));
 by (dres_inst_tac [("x","M")] spec 1);
 by (ultra_tac (claset(), simpset() addsimps [less_imp_le]) 1);

     auto_tac (claset(), simpset() addsimps [all_conj_distrib]));
 by (dtac choice 1 THEN 
     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);
 by (auto_tac (claset(), simpset() addsimps [hypreal_minus,
     hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));

 
 (***---------------------------------------------------------------
                  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,
         Bseq_NSBseq_iff RS sym, Bseq_iff1a]));
 qed "NSBseq_HFinite_hypreal";
 
 (*** 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(),
               simpset() addsimps [hypnat_omega_def, mem_infmal_iff RS sym,
                                   starfunNat,hypreal_of_real_zero]));