^^ -> ```
authornipkow
Fri Jan 05 18:48:18 2001 +0100 (2001-01-05)
changeset 10797028d22926a41
parent 10796 c0bcea781b3a
child 10798 0a1446ff6aff
^^ -> ```
Univalent -> single_valued
src/HOL/BCV/JType.ML
src/HOL/BCV/JVM.ML
src/HOL/BCV/Semilat.ML
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/Induct/Com.ML
src/HOL/Induct/Exp.ML
src/HOL/Integ/Equiv.ML
src/HOL/Integ/Equiv.thy
src/HOL/Integ/IntDef.ML
src/HOL/Integ/IntDef.thy
src/HOL/Lex/Automata.ML
src/HOL/Lex/Automata.thy
src/HOL/Lex/NAe.thy
src/HOL/MicroJava/BV/JType.thy
src/HOL/MicroJava/BV/Semilat.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/Relation.ML
src/HOL/Relation.thy
src/HOL/Relation_Power.ML
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/FP.ML
src/HOL/UNITY/PriorityAux.ML
src/HOL/UNITY/PriorityAux.thy
src/HOL/UNITY/Project.ML
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/WFair.ML
src/HOL/UNITY/WFair.thy
src/HOL/ex/Tarski.ML
src/HOL/ex/Tarski.thy
     1.1 --- a/src/HOL/BCV/JType.ML	Fri Jan 05 18:33:47 2001 +0100
     1.2 +++ b/src/HOL/BCV/JType.ML	Fri Jan 05 18:48:18 2001 +0100
     1.3 @@ -103,7 +103,7 @@
     1.4  Addsimps [is_type_def];
     1.5  
     1.6  Goalw [closed_def,plussub_def,lift2_def,err_def,JType.sup_def]
     1.7 - "[| univalent S; acyclic S |] ==> \
     1.8 + "[| single_valued S; acyclic S |] ==> \
     1.9  \ closed (err(types S)) (lift2 (JType.sup S))";
    1.10  by (simp_tac (simpset() addsplits [err.split,ty.split]) 1);
    1.11  by (blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD]
    1.12 @@ -113,7 +113,7 @@
    1.13  AddIffs [OK_le_conv];
    1.14  
    1.15  Goalw [semilat_def,split RS eq_reflection,JType.esl_def,Err.sl_def]
    1.16 - "[| univalent S; acyclic S |] ==> err_semilat (JType.esl S)";
    1.17 + "[| single_valued S; acyclic S |] ==> err_semilat (JType.esl S)";
    1.18  by (asm_full_simp_tac (simpset() addsimps [acyclic_impl_order_subtype,closed_err_types]) 1);
    1.19  
    1.20  by (rtac conjI 1);
     2.1 --- a/src/HOL/BCV/JVM.ML	Fri Jan 05 18:33:47 2001 +0100
     2.2 +++ b/src/HOL/BCV/JVM.ML	Fri Jan 05 18:48:18 2001 +0100
     2.3 @@ -229,7 +229,7 @@
     2.4  
     2.5  
     2.6  Goalw [JVM.sl_def,stk_esl_def,reg_sl_def]
     2.7 - "[| univalent S; acyclic S |] ==> semilat(JVM.sl S maxs maxr)";
     2.8 + "[| single_valued S; acyclic S |] ==> semilat(JVM.sl S maxs maxr)";
     2.9  by (REPEAT(ares_tac [semilat_opt,err_semilat_Product_esl,err_semilat_upto_esl,
    2.10            err_semilat_eslI,semilat_Listn_sl,err_semilat_JType_esl] 1));
    2.11  qed "semilat_JVM_slI";
    2.12 @@ -241,7 +241,7 @@
    2.13  qed "sl_triple_conv";
    2.14  
    2.15  Goalw [kiljvm_def,sl_triple_conv]
    2.16 - "[| univalent S; wf(S^-1); wfis S md maxr bs; wf_mdict S md; \
    2.17 + "[| single_valued S; wf(S^-1); wfis S md maxr bs; wf_mdict S md; \
    2.18  \    bounded (succs bs) (size bs) |] ==> \
    2.19  \ is_bcv (JVM.le S maxs maxr) (Some Err) (wti S maxs rT bs) \
    2.20  \        (size bs) (states S maxs maxr) (kiljvm S maxs maxr rT bs)";
     3.1 --- a/src/HOL/BCV/Semilat.ML	Fri Jan 05 18:33:47 2001 +0100
     3.2 +++ b/src/HOL/BCV/Semilat.ML	Fri Jan 05 18:48:18 2001 +0100
     3.3 @@ -136,21 +136,21 @@
     3.4  
     3.5  
     3.6  Goalw [is_lub_def,is_ub_def]
     3.7 - "[| univalent r; is_lub (r^*) x y u; (x',x) : r |] ==> \
     3.8 + "[| single_valued r; is_lub (r^*) x y u; (x',x) : r |] ==> \
     3.9  \    EX v. is_lub (r^*) x' y v";
    3.10  by (case_tac "(y,x) : r^*" 1);
    3.11   by (case_tac "(y,x') : r^*" 1);
    3.12    by (Blast_tac 1);
    3.13   by (blast_tac (claset() addIs [r_into_rtrancl] addEs [converse_rtranclE]
    3.14 -                        addDs [univalentD]) 1);
    3.15 +                        addDs [single_valuedD]) 1);
    3.16  by (rtac exI 1);
    3.17  by (rtac conjI 1);
    3.18 - by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]addDs [univalentD]) 1);
    3.19 + by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]addDs [single_valuedD]) 1);
    3.20  by (blast_tac (claset() addIs [rtrancl_into_rtrancl,rtrancl_into_rtrancl2]
    3.21 -                       addEs [converse_rtranclE] addDs [univalentD]) 1);
    3.22 +                       addEs [converse_rtranclE] addDs [single_valuedD]) 1);
    3.23  qed "extend_lub";
    3.24  
    3.25 -Goal "[| univalent r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> \
    3.26 +Goal "[| single_valued r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> \
    3.27  \     (EX z. is_lub (r^*) x y z))";
    3.28  by (etac converse_rtrancl_induct 1);
    3.29   by (Clarify_tac 1);
    3.30 @@ -158,7 +158,7 @@
    3.31    by (Blast_tac 1);
    3.32   by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
    3.33  by (blast_tac (claset() addIs [extend_lub]) 1);
    3.34 -qed_spec_mp "univalent_has_lubs";
    3.35 +qed_spec_mp "single_valued_has_lubs";
    3.36  
    3.37  Goalw [some_lub_def,is_lub_def]
    3.38   "[| acyclic r; is_lub (r^*) x y u |] ==> some_lub (r^*) x y = u";
    3.39 @@ -169,9 +169,9 @@
    3.40  qed "some_lub_conv";
    3.41  
    3.42  Goal
    3.43 - "[| univalent r; acyclic r; (x,u):r^*; (y,u):r^* |] ==> \
    3.44 + "[| single_valued r; acyclic r; (x,u):r^*; (y,u):r^* |] ==> \
    3.45  \ is_lub (r^*) x y (some_lub (r^*) x y)";
    3.46  by (fast_tac
    3.47 -    (claset() addDs [univalent_has_lubs]
    3.48 +    (claset() addDs [single_valued_has_lubs]
    3.49       addss (simpset() addsimps [some_lub_conv])) 1);
    3.50  qed "is_lub_some_lub";
     4.1 --- a/src/HOL/Hyperreal/HRealAbs.ML	Fri Jan 05 18:33:47 2001 +0100
     4.2 +++ b/src/HOL/Hyperreal/HRealAbs.ML	Fri Jan 05 18:48:18 2001 +0100
     4.3 @@ -19,8 +19,8 @@
     4.4  Addsimps [hrabs_number_of];
     4.5  
     4.6  Goalw [hrabs_def]
     4.7 -     "abs (Abs_hypreal (hyprel ^^ {X})) = \
     4.8 -\     Abs_hypreal(hyprel ^^ {%n. abs (X n)})";
     4.9 +     "abs (Abs_hypreal (hyprel ``` {X})) = \
    4.10 +\     Abs_hypreal(hyprel ``` {%n. abs (X n)})";
    4.11  by (auto_tac (claset(),
    4.12                simpset_of HyperDef.thy 
    4.13                    addsimps [hypreal_zero_def, hypreal_le,hypreal_minus]));
    4.14 @@ -232,7 +232,7 @@
    4.15  (*------------------------------------------------------------*)
    4.16  
    4.17  Goalw [hypreal_of_nat_def, hypreal_of_real_def, real_of_nat_def] 
    4.18 -     "hypreal_of_nat  m = Abs_hypreal(hyprel^^{%n. real_of_nat m})";
    4.19 +     "hypreal_of_nat  m = Abs_hypreal(hyprel```{%n. real_of_nat m})";
    4.20  by Auto_tac;
    4.21  qed "hypreal_of_nat_iff";
    4.22  
     5.1 --- a/src/HOL/Hyperreal/HSeries.ML	Fri Jan 05 18:33:47 2001 +0100
     5.2 +++ b/src/HOL/Hyperreal/HSeries.ML	Fri Jan 05 18:48:18 2001 +0100
     5.3 @@ -8,14 +8,14 @@
     5.4  Goalw [sumhr_def]
     5.5       "sumhr(M,N,f) =  \
     5.6  \       Abs_hypreal(UN X:Rep_hypnat(M). UN Y: Rep_hypnat(N). \
     5.7 -\         hyprel ^^{%n::nat. sumr (X n) (Y n) f})";
     5.8 +\         hyprel ```{%n::nat. sumr (X n) (Y n) f})";
     5.9  by (Auto_tac);
    5.10  qed "sumhr_iff";
    5.11  
    5.12  Goalw [sumhr_def]
    5.13 -     "sumhr(Abs_hypnat(hypnatrel^^{%n. M n}), \
    5.14 -\           Abs_hypnat(hypnatrel^^{%n. N n}), f) = \
    5.15 -\     Abs_hypreal(hyprel ^^ {%n. sumr (M n) (N n) f})";
    5.16 +     "sumhr(Abs_hypnat(hypnatrel```{%n. M n}), \
    5.17 +\           Abs_hypnat(hypnatrel```{%n. N n}), f) = \
    5.18 +\     Abs_hypreal(hyprel ``` {%n. sumr (M n) (N n) f})";
    5.19  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
    5.20  by (Auto_tac THEN Ultra_tac 1);
    5.21  qed "sumhr";
    5.22 @@ -27,7 +27,7 @@
    5.23  Goalw [sumhr_def]
    5.24        "sumhr p = (%(M,N,f). Abs_hypreal(UN X:Rep_hypnat(M). \
    5.25  \                     UN Y: Rep_hypnat(N). \
    5.26 -\           hyprel ^^{%n::nat. sumr (X n) (Y n) f})) p";
    5.27 +\           hyprel ```{%n::nat. sumr (X n) (Y n) f})) p";
    5.28  by (res_inst_tac [("p","p")] PairE 1);
    5.29  by (res_inst_tac [("p","y")] PairE 1);
    5.30  by (Auto_tac);
     6.1 --- a/src/HOL/Hyperreal/HSeries.thy	Fri Jan 05 18:33:47 2001 +0100
     6.2 +++ b/src/HOL/Hyperreal/HSeries.thy	Fri Jan 05 18:48:18 2001 +0100
     6.3 @@ -15,7 +15,7 @@
     6.4     "sumhr p
     6.5         == Abs_hypreal(UN X:Rep_hypnat(fst p). 
     6.6                UN Y: Rep_hypnat(fst(snd p)).
     6.7 -              hyprel ^^{%n::nat. sumr (X n) (Y n) (snd(snd p))})"
     6.8 +              hyprel```{%n::nat. sumr (X n) (Y n) (snd(snd p))})"
     6.9  
    6.10  constdefs
    6.11     NSsums  :: [nat=>real,real] => bool     (infixr 80)
     7.1 --- a/src/HOL/Hyperreal/HyperDef.ML	Fri Jan 05 18:33:47 2001 +0100
     7.2 +++ b/src/HOL/Hyperreal/HyperDef.ML	Fri Jan 05 18:48:18 2001 +0100
     7.3 @@ -206,11 +206,11 @@
     7.4  	      simpset() addsimps [FreeUltrafilterNat_Nat_set]));
     7.5  qed "equiv_hyprel";
     7.6  
     7.7 -(* (hyprel ^^ {x} = hyprel ^^ {y}) = ((x,y) : hyprel) *)
     7.8 +(* (hyprel ``` {x} = hyprel ``` {y}) = ((x,y) : hyprel) *)
     7.9  bind_thm ("equiv_hyprel_iff",
    7.10      	  [equiv_hyprel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
    7.11  
    7.12 -Goalw  [hypreal_def,hyprel_def,quotient_def] "hyprel^^{x}:hypreal";
    7.13 +Goalw  [hypreal_def,hyprel_def,quotient_def] "hyprel```{x}:hypreal";
    7.14  by (Blast_tac 1);
    7.15  qed "hyprel_in_hypreal";
    7.16  
    7.17 @@ -230,7 +230,7 @@
    7.18  by (rtac Rep_hypreal_inverse 1);
    7.19  qed "inj_Rep_hypreal";
    7.20  
    7.21 -Goalw [hyprel_def] "x: hyprel ^^ {x}";
    7.22 +Goalw [hyprel_def] "x: hyprel ``` {x}";
    7.23  by (Step_tac 1);
    7.24  by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset()));
    7.25  qed "lemma_hyprel_refl";
    7.26 @@ -267,7 +267,7 @@
    7.27  qed "inj_hypreal_of_real";
    7.28  
    7.29  val [prem] = goal (the_context ())
    7.30 -    "(!!x y. z = Abs_hypreal(hyprel^^{x}) ==> P) ==> P";
    7.31 +    "(!!x y. z = Abs_hypreal(hyprel```{x}) ==> P) ==> P";
    7.32  by (res_inst_tac [("x1","z")] 
    7.33      (rewrite_rule [hypreal_def] Rep_hypreal RS quotientE) 1);
    7.34  by (dres_inst_tac [("f","Abs_hypreal")] arg_cong 1);
    7.35 @@ -278,13 +278,13 @@
    7.36  (**** hypreal_minus: additive inverse on hypreal ****)
    7.37  
    7.38  Goalw [congruent_def]
    7.39 -  "congruent hyprel (%X. hyprel^^{%n. - (X n)})";
    7.40 +  "congruent hyprel (%X. hyprel```{%n. - (X n)})";
    7.41  by Safe_tac;
    7.42  by (ALLGOALS Ultra_tac);
    7.43  qed "hypreal_minus_congruent";
    7.44  
    7.45  Goalw [hypreal_minus_def]
    7.46 -   "- (Abs_hypreal(hyprel^^{%n. X n})) = Abs_hypreal(hyprel ^^ {%n. -(X n)})";
    7.47 +   "- (Abs_hypreal(hyprel```{%n. X n})) = Abs_hypreal(hyprel ``` {%n. -(X n)})";
    7.48  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
    7.49  by (simp_tac (simpset() addsimps 
    7.50        [hyprel_in_hypreal RS Abs_hypreal_inverse,
    7.51 @@ -322,20 +322,20 @@
    7.52  (**** hyperreal addition: hypreal_add  ****)
    7.53  
    7.54  Goalw [congruent2_def]
    7.55 -    "congruent2 hyprel (%X Y. hyprel^^{%n. X n + Y n})";
    7.56 +    "congruent2 hyprel (%X Y. hyprel```{%n. X n + Y n})";
    7.57  by Safe_tac;
    7.58  by (ALLGOALS(Ultra_tac));
    7.59  qed "hypreal_add_congruent2";
    7.60  
    7.61  Goalw [hypreal_add_def]
    7.62 -  "Abs_hypreal(hyprel^^{%n. X n}) + Abs_hypreal(hyprel^^{%n. Y n}) = \
    7.63 -\  Abs_hypreal(hyprel^^{%n. X n + Y n})";
    7.64 +  "Abs_hypreal(hyprel```{%n. X n}) + Abs_hypreal(hyprel```{%n. Y n}) = \
    7.65 +\  Abs_hypreal(hyprel```{%n. X n + Y n})";
    7.66  by (simp_tac (simpset() addsimps 
    7.67           [[equiv_hyprel, hypreal_add_congruent2] MRS UN_equiv_class2]) 1);
    7.68  qed "hypreal_add";
    7.69  
    7.70 -Goal "Abs_hypreal(hyprel^^{%n. X n}) - Abs_hypreal(hyprel^^{%n. Y n}) = \
    7.71 -\     Abs_hypreal(hyprel^^{%n. X n - Y n})";
    7.72 +Goal "Abs_hypreal(hyprel```{%n. X n}) - Abs_hypreal(hyprel```{%n. Y n}) = \
    7.73 +\     Abs_hypreal(hyprel```{%n. X n - Y n})";
    7.74  by (simp_tac (simpset() addsimps 
    7.75           [hypreal_diff_def, hypreal_minus,hypreal_add]) 1);
    7.76  qed "hypreal_diff";
    7.77 @@ -496,14 +496,14 @@
    7.78  (**** hyperreal multiplication: hypreal_mult  ****)
    7.79  
    7.80  Goalw [congruent2_def]
    7.81 -    "congruent2 hyprel (%X Y. hyprel^^{%n. X n * Y n})";
    7.82 +    "congruent2 hyprel (%X Y. hyprel```{%n. X n * Y n})";
    7.83  by Safe_tac;
    7.84  by (ALLGOALS(Ultra_tac));
    7.85  qed "hypreal_mult_congruent2";
    7.86  
    7.87  Goalw [hypreal_mult_def]
    7.88 -  "Abs_hypreal(hyprel^^{%n. X n}) * Abs_hypreal(hyprel^^{%n. Y n}) = \
    7.89 -\  Abs_hypreal(hyprel^^{%n. X n * Y n})";
    7.90 +  "Abs_hypreal(hyprel```{%n. X n}) * Abs_hypreal(hyprel```{%n. Y n}) = \
    7.91 +\  Abs_hypreal(hyprel```{%n. X n * Y n})";
    7.92  by (simp_tac (simpset() addsimps 
    7.93        [[equiv_hyprel, hypreal_mult_congruent2] MRS UN_equiv_class2]) 1);
    7.94  qed "hypreal_mult";
    7.95 @@ -622,13 +622,13 @@
    7.96  (**** multiplicative inverse on hypreal ****)
    7.97  
    7.98  Goalw [congruent_def]
    7.99 -  "congruent hyprel (%X. hyprel^^{%n. if X n = #0 then #0 else inverse(X n)})";
   7.100 +  "congruent hyprel (%X. hyprel```{%n. if X n = #0 then #0 else inverse(X n)})";
   7.101  by (Auto_tac THEN Ultra_tac 1);
   7.102  qed "hypreal_inverse_congruent";
   7.103  
   7.104  Goalw [hypreal_inverse_def]
   7.105 -      "inverse (Abs_hypreal(hyprel^^{%n. X n})) = \
   7.106 -\      Abs_hypreal(hyprel ^^ {%n. if X n = #0 then #0 else inverse(X n)})";
   7.107 +      "inverse (Abs_hypreal(hyprel```{%n. X n})) = \
   7.108 +\      Abs_hypreal(hyprel ``` {%n. if X n = #0 then #0 else inverse(X n)})";
   7.109  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   7.110  by (simp_tac (simpset() addsimps 
   7.111     [hyprel_in_hypreal RS Abs_hypreal_inverse,
   7.112 @@ -800,8 +800,8 @@
   7.113    makes many of them more straightforward. 
   7.114   -------------------------------------------------------*)
   7.115  Goalw [hypreal_less_def]
   7.116 -      "(Abs_hypreal(hyprel^^{%n. X n}) < \
   7.117 -\           Abs_hypreal(hyprel^^{%n. Y n})) = \
   7.118 +      "(Abs_hypreal(hyprel```{%n. X n}) < \
   7.119 +\           Abs_hypreal(hyprel```{%n. Y n})) = \
   7.120  \      ({n. X n < Y n} : FreeUltrafilterNat)";
   7.121  by (auto_tac (claset() addSIs [lemma_hyprel_refl], simpset()));
   7.122  by (Ultra_tac 1);
   7.123 @@ -840,7 +840,7 @@
   7.124                           Trichotomy of the hyperreals
   7.125    --------------------------------------------------------------------------------*)
   7.126  
   7.127 -Goalw [hyprel_def] "EX x. x: hyprel ^^ {%n. #0}";
   7.128 +Goalw [hyprel_def] "EX x. x: hyprel ``` {%n. #0}";
   7.129  by (res_inst_tac [("x","%n. #0")] exI 1);
   7.130  by (Step_tac 1);
   7.131  by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset()));
   7.132 @@ -958,8 +958,8 @@
   7.133  (*------ hypreal le iff reals le a.e ------*)
   7.134  
   7.135  Goalw [hypreal_le_def,real_le_def]
   7.136 -      "(Abs_hypreal(hyprel^^{%n. X n}) <= \
   7.137 -\           Abs_hypreal(hyprel^^{%n. Y n})) = \
   7.138 +      "(Abs_hypreal(hyprel```{%n. X n}) <= \
   7.139 +\           Abs_hypreal(hyprel```{%n. Y n})) = \
   7.140  \      ({n. X n <= Y n} : FreeUltrafilterNat)";
   7.141  by (auto_tac (claset(),simpset() addsimps [hypreal_less]));
   7.142  by (ALLGOALS(Ultra_tac));
     8.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Fri Jan 05 18:33:47 2001 +0100
     8.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Fri Jan 05 18:48:18 2001 +0100
     8.3 @@ -37,28 +37,28 @@
     8.4  defs
     8.5  
     8.6    hypreal_zero_def
     8.7 -  "0 == Abs_hypreal(hyprel^^{%n::nat. (#0::real)})"
     8.8 +  "0 == Abs_hypreal(hyprel```{%n::nat. (#0::real)})"
     8.9  
    8.10    hypreal_one_def
    8.11 -  "1hr == Abs_hypreal(hyprel^^{%n::nat. (#1::real)})"
    8.12 +  "1hr == Abs_hypreal(hyprel```{%n::nat. (#1::real)})"
    8.13  
    8.14    (* an infinite number = [<1,2,3,...>] *)
    8.15    omega_def
    8.16 -  "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_nat (Suc n)})"
    8.17 +  "whr == Abs_hypreal(hyprel```{%n::nat. real_of_nat (Suc n)})"
    8.18      
    8.19    (* an infinitesimal number = [<1,1/2,1/3,...>] *)
    8.20    epsilon_def
    8.21 -  "ehr == Abs_hypreal(hyprel^^{%n::nat. inverse (real_of_nat (Suc n))})"
    8.22 +  "ehr == Abs_hypreal(hyprel```{%n::nat. inverse (real_of_nat (Suc n))})"
    8.23  
    8.24    hypreal_minus_def
    8.25 -  "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel^^{%n::nat. - (X n)})"
    8.26 +  "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel```{%n::nat. - (X n)})"
    8.27  
    8.28    hypreal_diff_def 
    8.29    "x - y == x + -(y::hypreal)"
    8.30  
    8.31    hypreal_inverse_def
    8.32    "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). 
    8.33 -                    hyprel^^{%n. if X n = #0 then #0 else inverse (X n)})"
    8.34 +                    hyprel```{%n. if X n = #0 then #0 else inverse (X n)})"
    8.35  
    8.36    hypreal_divide_def
    8.37    "P / Q::hypreal == P * inverse Q"
    8.38 @@ -66,17 +66,17 @@
    8.39  constdefs
    8.40  
    8.41    hypreal_of_real  :: real => hypreal                 
    8.42 -  "hypreal_of_real r         == Abs_hypreal(hyprel^^{%n::nat. r})"
    8.43 +  "hypreal_of_real r         == Abs_hypreal(hyprel```{%n::nat. r})"
    8.44  
    8.45  defs 
    8.46  
    8.47    hypreal_add_def  
    8.48    "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
    8.49 -                hyprel^^{%n::nat. X n + Y n})"
    8.50 +                hyprel```{%n::nat. X n + Y n})"
    8.51  
    8.52    hypreal_mult_def  
    8.53    "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
    8.54 -                hyprel^^{%n::nat. X n * Y n})"
    8.55 +                hyprel```{%n::nat. X n * Y n})"
    8.56  
    8.57    hypreal_less_def
    8.58    "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & 
     9.1 --- a/src/HOL/Hyperreal/HyperNat.ML	Fri Jan 05 18:33:47 2001 +0100
     9.2 +++ b/src/HOL/Hyperreal/HyperNat.ML	Fri Jan 05 18:48:18 2001 +0100
     9.3 @@ -65,7 +65,7 @@
     9.4  val equiv_hypnatrel_iff =
     9.5      [UNIV_I, UNIV_I] MRS (equiv_hypnatrel RS eq_equiv_class_iff);
     9.6  
     9.7 -Goalw  [hypnat_def,hypnatrel_def,quotient_def] "hypnatrel^^{x}:hypnat";
     9.8 +Goalw  [hypnat_def,hypnatrel_def,quotient_def] "hypnatrel```{x}:hypnat";
     9.9  by (Blast_tac 1);
    9.10  qed "hypnatrel_in_hypnat";
    9.11  
    9.12 @@ -85,7 +85,7 @@
    9.13  by (rtac Rep_hypnat_inverse 1);
    9.14  qed "inj_Rep_hypnat";
    9.15  
    9.16 -Goalw [hypnatrel_def] "x: hypnatrel ^^ {x}";
    9.17 +Goalw [hypnatrel_def] "x: hypnatrel ``` {x}";
    9.18  by (Step_tac 1);
    9.19  by Auto_tac;
    9.20  qed "lemma_hypnatrel_refl";
    9.21 @@ -121,7 +121,7 @@
    9.22  qed "inj_hypnat_of_nat";
    9.23  
    9.24  val [prem] = Goal
    9.25 -    "(!!x. z = Abs_hypnat(hypnatrel^^{x}) ==> P) ==> P";
    9.26 +    "(!!x. z = Abs_hypnat(hypnatrel```{x}) ==> P) ==> P";
    9.27  by (res_inst_tac [("x1","z")] 
    9.28      (rewrite_rule [hypnat_def] Rep_hypnat RS quotientE) 1);
    9.29  by (dres_inst_tac [("f","Abs_hypnat")] arg_cong 1);
    9.30 @@ -133,14 +133,14 @@
    9.31     Addition for hyper naturals: hypnat_add 
    9.32   -----------------------------------------------------------*)
    9.33  Goalw [congruent2_def]
    9.34 -     "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n + Y n})";
    9.35 +     "congruent2 hypnatrel (%X Y. hypnatrel```{%n. X n + Y n})";
    9.36  by Safe_tac;
    9.37  by (ALLGOALS(Fuf_tac));
    9.38  qed "hypnat_add_congruent2";
    9.39  
    9.40  Goalw [hypnat_add_def]
    9.41 -  "Abs_hypnat(hypnatrel^^{%n. X n}) + Abs_hypnat(hypnatrel^^{%n. Y n}) = \
    9.42 -\  Abs_hypnat(hypnatrel^^{%n. X n + Y n})";
    9.43 +  "Abs_hypnat(hypnatrel```{%n. X n}) + Abs_hypnat(hypnatrel```{%n. Y n}) = \
    9.44 +\  Abs_hypnat(hypnatrel```{%n. X n + Y n})";
    9.45  by (asm_simp_tac
    9.46      (simpset() addsimps [[equiv_hypnatrel, hypnat_add_congruent2] 
    9.47       MRS UN_equiv_class2]) 1);
    9.48 @@ -186,14 +186,14 @@
    9.49     Subtraction for hyper naturals: hypnat_minus
    9.50   -----------------------------------------------------------*)
    9.51  Goalw [congruent2_def]
    9.52 -    "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n - Y n})";
    9.53 +    "congruent2 hypnatrel (%X Y. hypnatrel```{%n. X n - Y n})";
    9.54  by Safe_tac;
    9.55  by (ALLGOALS(Fuf_tac));
    9.56  qed "hypnat_minus_congruent2";
    9.57   
    9.58  Goalw [hypnat_minus_def]
    9.59 -  "Abs_hypnat(hypnatrel^^{%n. X n}) - Abs_hypnat(hypnatrel^^{%n. Y n}) = \
    9.60 -\  Abs_hypnat(hypnatrel^^{%n. X n - Y n})";
    9.61 +  "Abs_hypnat(hypnatrel```{%n. X n}) - Abs_hypnat(hypnatrel```{%n. Y n}) = \
    9.62 +\  Abs_hypnat(hypnatrel```{%n. X n - Y n})";
    9.63  by (asm_simp_tac
    9.64      (simpset() addsimps [[equiv_hypnatrel, hypnat_minus_congruent2] 
    9.65       MRS UN_equiv_class2]) 1);
    9.66 @@ -273,14 +273,14 @@
    9.67     Multiplication for hyper naturals: hypnat_mult
    9.68   -----------------------------------------------------------*)
    9.69  Goalw [congruent2_def]
    9.70 -    "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n * Y n})";
    9.71 +    "congruent2 hypnatrel (%X Y. hypnatrel```{%n. X n * Y n})";
    9.72  by Safe_tac;
    9.73  by (ALLGOALS(Fuf_tac));
    9.74  qed "hypnat_mult_congruent2";
    9.75  
    9.76  Goalw [hypnat_mult_def]
    9.77 -  "Abs_hypnat(hypnatrel^^{%n. X n}) * Abs_hypnat(hypnatrel^^{%n. Y n}) = \
    9.78 -\  Abs_hypnat(hypnatrel^^{%n. X n * Y n})";
    9.79 +  "Abs_hypnat(hypnatrel```{%n. X n}) * Abs_hypnat(hypnatrel```{%n. Y n}) = \
    9.80 +\  Abs_hypnat(hypnatrel```{%n. X n * Y n})";
    9.81  by (asm_simp_tac
    9.82      (simpset() addsimps [[equiv_hypnatrel,hypnat_mult_congruent2] MRS
    9.83       UN_equiv_class2]) 1);
    9.84 @@ -475,8 +475,8 @@
    9.85  (* See comments in HYPER for corresponding thm *)
    9.86  
    9.87  Goalw [hypnat_less_def]
    9.88 -      "(Abs_hypnat(hypnatrel^^{%n. X n}) < \
    9.89 -\           Abs_hypnat(hypnatrel^^{%n. Y n})) = \
    9.90 +      "(Abs_hypnat(hypnatrel```{%n. X n}) < \
    9.91 +\           Abs_hypnat(hypnatrel```{%n. Y n})) = \
    9.92  \      ({n. X n < Y n} : FreeUltrafilterNat)";
    9.93  by (auto_tac (claset() addSIs [lemma_hypnatrel_refl],simpset()));
    9.94  by (Fuf_tac 1);
    9.95 @@ -527,7 +527,7 @@
    9.96  (*---------------------------------------------------------------------------------
    9.97                     Trichotomy of the hyper naturals
    9.98    --------------------------------------------------------------------------------*)
    9.99 -Goalw [hypnatrel_def] "EX x. x: hypnatrel ^^ {%n. 0}";
   9.100 +Goalw [hypnatrel_def] "EX x. x: hypnatrel ``` {%n. 0}";
   9.101  by (res_inst_tac [("x","%n. 0")] exI 1);
   9.102  by (Step_tac 1);
   9.103  by Auto_tac;
   9.104 @@ -620,8 +620,8 @@
   9.105  
   9.106  (*------ hypnat le iff nat le a.e ------*)
   9.107  Goalw [hypnat_le_def,le_def]
   9.108 -      "(Abs_hypnat(hypnatrel^^{%n. X n}) <= \
   9.109 -\           Abs_hypnat(hypnatrel^^{%n. Y n})) = \
   9.110 +      "(Abs_hypnat(hypnatrel```{%n. X n}) <= \
   9.111 +\           Abs_hypnat(hypnatrel```{%n. Y n})) = \
   9.112  \      ({n. X n <= Y n} : FreeUltrafilterNat)";
   9.113  by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
   9.114      simpset() addsimps [hypnat_less]));
   9.115 @@ -833,7 +833,7 @@
   9.116                Existence of infinite hypernatural number
   9.117   ---------------------------------------------------------------------------------*)
   9.118  
   9.119 -Goal "hypnatrel^^{%n::nat. n} : hypnat";
   9.120 +Goal "hypnatrel```{%n::nat. n} : hypnat";
   9.121  by Auto_tac;
   9.122  qed "hypnat_omega";
   9.123  
   9.124 @@ -1066,7 +1066,7 @@
   9.125       "HNatInfinite = {N. ALL n:SNat. n < N}";
   9.126  by (Step_tac 1);
   9.127  by (dres_inst_tac [("x","Abs_hypnat \
   9.128 -\        (hypnatrel ^^ {%n. N})")] bspec 2);
   9.129 +\        (hypnatrel ``` {%n. N})")] bspec 2);
   9.130  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   9.131  by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   9.132  by (auto_tac (claset(),simpset() addsimps [hypnat_less_iff]));
   9.133 @@ -1215,14 +1215,14 @@
   9.134      Embedding of the hypernaturals into the hyperreal
   9.135   --------------------------------------------------------------*)
   9.136  
   9.137 -Goal "(Ya : hyprel ^^{%n. f(n)}) = \
   9.138 +Goal "(Ya : hyprel ```{%n. f(n)}) = \
   9.139  \     ({n. f n = Ya n} : FreeUltrafilterNat)";
   9.140  by Auto_tac;
   9.141  qed "lemma_hyprel_FUFN";
   9.142  
   9.143  Goalw [hypreal_of_hypnat_def]
   9.144 -      "hypreal_of_hypnat (Abs_hypnat(hypnatrel^^{%n. X n})) = \
   9.145 -\         Abs_hypreal(hyprel ^^ {%n. real_of_nat (X n)})";
   9.146 +      "hypreal_of_hypnat (Abs_hypnat(hypnatrel```{%n. X n})) = \
   9.147 +\         Abs_hypreal(hyprel ``` {%n. real_of_nat (X n)})";
   9.148  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   9.149  by (auto_tac (claset()
   9.150                    addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset],
    10.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Fri Jan 05 18:33:47 2001 +0100
    10.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Fri Jan 05 18:48:18 2001 +0100
    10.3 @@ -25,7 +25,7 @@
    10.4  
    10.5    (* embedding the naturals in the hypernaturals *)
    10.6    hypnat_of_nat   :: nat => hypnat
    10.7 -  "hypnat_of_nat m  == Abs_hypnat(hypnatrel^^{%n::nat. m})"
    10.8 +  "hypnat_of_nat m  == Abs_hypnat(hypnatrel```{%n::nat. m})"
    10.9  
   10.10    (* hypernaturals as members of the hyperreals; the set is defined as  *)
   10.11    (* the nonstandard extension of set of naturals embedded in the reals *)
   10.12 @@ -39,7 +39,7 @@
   10.13    (* explicit embedding of the hypernaturals in the hyperreals *)    
   10.14    hypreal_of_hypnat :: hypnat => hypreal
   10.15    "hypreal_of_hypnat N  == Abs_hypreal(UN X: Rep_hypnat(N). 
   10.16 -                            hyprel^^{%n::nat. real_of_nat (X n)})"
   10.17 +                            hyprel```{%n::nat. real_of_nat (X n)})"
   10.18    
   10.19  defs
   10.20  
   10.21 @@ -53,23 +53,23 @@
   10.22  
   10.23    (** hypernatural arithmetic **)
   10.24    
   10.25 -  hypnat_zero_def      "0 == Abs_hypnat(hypnatrel^^{%n::nat. 0})"
   10.26 -  hypnat_one_def       "1hn == Abs_hypnat(hypnatrel^^{%n::nat. 1})"
   10.27 +  hypnat_zero_def      "0 == Abs_hypnat(hypnatrel```{%n::nat. 0})"
   10.28 +  hypnat_one_def       "1hn == Abs_hypnat(hypnatrel```{%n::nat. 1})"
   10.29  
   10.30    (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
   10.31 -  hypnat_omega_def     "whn == Abs_hypnat(hypnatrel^^{%n::nat. n})"
   10.32 +  hypnat_omega_def     "whn == Abs_hypnat(hypnatrel```{%n::nat. n})"
   10.33   
   10.34    hypnat_add_def  
   10.35    "P + Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
   10.36 -                hypnatrel^^{%n::nat. X n + Y n})"
   10.37 +                hypnatrel```{%n::nat. X n + Y n})"
   10.38  
   10.39    hypnat_mult_def  
   10.40    "P * Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
   10.41 -                hypnatrel^^{%n::nat. X n * Y n})"
   10.42 +                hypnatrel```{%n::nat. X n * Y n})"
   10.43  
   10.44    hypnat_minus_def  
   10.45    "P - Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
   10.46 -                hypnatrel^^{%n::nat. X n - Y n})"
   10.47 +                hypnatrel```{%n::nat. X n - Y n})"
   10.48  
   10.49    hypnat_less_def
   10.50    "P < (Q::hypnat) == EX X Y. X: Rep_hypnat(P) & 
    11.1 --- a/src/HOL/Hyperreal/HyperPow.ML	Fri Jan 05 18:33:47 2001 +0100
    11.2 +++ b/src/HOL/Hyperreal/HyperPow.ML	Fri Jan 05 18:48:18 2001 +0100
    11.3 @@ -178,7 +178,7 @@
    11.4                simpset() addsimps [hypreal_mult_less_mono2]));
    11.5  qed_spec_mp "hrealpow_Suc_le";
    11.6  
    11.7 -Goal "Abs_hypreal(hyprel^^{%n. X n}) ^ m = Abs_hypreal(hyprel^^{%n. (X n) ^ m})";
    11.8 +Goal "Abs_hypreal(hyprel```{%n. X n}) ^ m = Abs_hypreal(hyprel```{%n. (X n) ^ m})";
    11.9  by (induct_tac "m" 1);
   11.10  by (auto_tac (claset(),
   11.11                simpset() delsimps [one_eq_numeral_1]
   11.12 @@ -221,14 +221,14 @@
   11.13   --------------------------------------------------------------*)
   11.14  Goalw [congruent_def]
   11.15       "congruent hyprel \
   11.16 -\    (%X Y. hyprel^^{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})";
   11.17 +\    (%X Y. hyprel```{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})";
   11.18  by (safe_tac (claset() addSIs [ext]));
   11.19  by (ALLGOALS(Fuf_tac));
   11.20  qed "hyperpow_congruent";
   11.21  
   11.22  Goalw [hyperpow_def]
   11.23 -  "Abs_hypreal(hyprel^^{%n. X n}) pow Abs_hypnat(hypnatrel^^{%n. Y n}) = \
   11.24 -\  Abs_hypreal(hyprel^^{%n. X n ^ Y n})";
   11.25 +  "Abs_hypreal(hyprel```{%n. X n}) pow Abs_hypnat(hypnatrel```{%n. Y n}) = \
   11.26 +\  Abs_hypreal(hyprel```{%n. X n ^ Y n})";
   11.27  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   11.28  by (auto_tac (claset() addSIs [lemma_hyprel_refl,bexI],
   11.29      simpset() addsimps [hyprel_in_hypreal RS 
    12.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Fri Jan 05 18:33:47 2001 +0100
    12.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Fri Jan 05 18:48:18 2001 +0100
    12.3 @@ -32,5 +32,5 @@
    12.4    hyperpow_def
    12.5    "(R::hypreal) pow (N::hypnat) 
    12.6        == Abs_hypreal(UN X:Rep_hypreal(R). UN Y: Rep_hypnat(N).
    12.7 -             hyprel^^{%n::nat. (X n) ^ (Y n)})"
    12.8 +             hyprel```{%n::nat. (X n) ^ (Y n)})"
    12.9  end
    13.1 --- a/src/HOL/Hyperreal/Lim.ML	Fri Jan 05 18:33:47 2001 +0100
    13.2 +++ b/src/HOL/Hyperreal/Lim.ML	Fri Jan 05 18:48:18 2001 +0100
    13.3 @@ -220,7 +220,7 @@
    13.4  by (fold_tac [real_le_def]);
    13.5  by (dtac lemma_skolemize_LIM2 1);
    13.6  by (Step_tac 1);
    13.7 -by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{X})")] spec 1);
    13.8 +by (dres_inst_tac [("x","Abs_hypreal(hyprel```{X})")] spec 1);
    13.9  by (asm_full_simp_tac
   13.10      (simpset() addsimps [starfun, hypreal_minus, 
   13.11                           hypreal_of_real_def,hypreal_add]) 1);
   13.12 @@ -726,8 +726,8 @@
   13.13  by (fold_tac [real_le_def]);
   13.14  by (dtac lemma_skolemize_LIM2u 1);
   13.15  by (Step_tac 1);
   13.16 -by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{X})")] spec 1);
   13.17 -by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{Y})")] spec 1);
   13.18 +by (dres_inst_tac [("x","Abs_hypreal(hyprel```{X})")] spec 1);
   13.19 +by (dres_inst_tac [("x","Abs_hypreal(hyprel```{Y})")] spec 1);
   13.20  by (asm_full_simp_tac
   13.21      (simpset() addsimps [starfun, hypreal_minus,hypreal_add]) 1);
   13.22  by Auto_tac;
    14.1 --- a/src/HOL/Hyperreal/NSA.ML	Fri Jan 05 18:33:47 2001 +0100
    14.2 +++ b/src/HOL/Hyperreal/NSA.ML	Fri Jan 05 18:48:18 2001 +0100
    14.3 @@ -2059,7 +2059,7 @@
    14.4         Omega is a member of HInfinite
    14.5   -----------------------------------------------*)
    14.6  
    14.7 -Goal "hyprel^^{%n::nat. real_of_nat (Suc n)} : hypreal";
    14.8 +Goal "hyprel```{%n::nat. real_of_nat (Suc n)} : hypreal";
    14.9  by Auto_tac;
   14.10  qed "hypreal_omega";
   14.11  
   14.12 @@ -2192,7 +2192,7 @@
   14.13      |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x|: Infinitesimal 
   14.14   -----------------------------------------------------*)
   14.15  Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \ 
   14.16 -\    ==> Abs_hypreal(hyprel^^{X}) + -hypreal_of_real x : Infinitesimal";
   14.17 +\    ==> Abs_hypreal(hyprel```{X}) + -hypreal_of_real x : Infinitesimal";
   14.18  by (auto_tac (claset() addSIs [bexI] 
   14.19             addDs [rename_numerals FreeUltrafilterNat_inverse_real_of_posnat,
   14.20                    FreeUltrafilterNat_all,FreeUltrafilterNat_Int] 
   14.21 @@ -2203,21 +2203,21 @@
   14.22  qed "real_seq_to_hypreal_Infinitesimal";
   14.23  
   14.24  Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \ 
   14.25 -\     ==> Abs_hypreal(hyprel^^{X}) @= hypreal_of_real x";
   14.26 +\     ==> Abs_hypreal(hyprel```{X}) @= hypreal_of_real x";
   14.27  by (rtac (inf_close_minus_iff RS ssubst) 1);
   14.28  by (rtac (mem_infmal_iff RS subst) 1);
   14.29  by (etac real_seq_to_hypreal_Infinitesimal 1);
   14.30  qed "real_seq_to_hypreal_inf_close";
   14.31  
   14.32  Goal "ALL n. abs(x + -X n) < inverse(real_of_nat(Suc n)) \ 
   14.33 -\              ==> Abs_hypreal(hyprel^^{X}) @= hypreal_of_real x";
   14.34 +\              ==> Abs_hypreal(hyprel```{X}) @= hypreal_of_real x";
   14.35  by (asm_full_simp_tac (simpset() addsimps [abs_minus_add_cancel,
   14.36          real_seq_to_hypreal_inf_close]) 1);
   14.37  qed "real_seq_to_hypreal_inf_close2";
   14.38  
   14.39  Goal "ALL n. abs(X n + -Y n) < inverse(real_of_nat(Suc n)) \ 
   14.40 -\     ==> Abs_hypreal(hyprel^^{X}) + \
   14.41 -\         -Abs_hypreal(hyprel^^{Y}) : Infinitesimal";
   14.42 +\     ==> Abs_hypreal(hyprel```{X}) + \
   14.43 +\         -Abs_hypreal(hyprel```{Y}) : Infinitesimal";
   14.44  by (auto_tac (claset() addSIs [bexI] 
   14.45                    addDs [rename_numerals 
   14.46                           FreeUltrafilterNat_inverse_real_of_posnat,
    15.1 --- a/src/HOL/Hyperreal/NatStar.ML	Fri Jan 05 18:33:47 2001 +0100
    15.2 +++ b/src/HOL/Hyperreal/NatStar.ML	Fri Jan 05 18:48:18 2001 +0100
    15.3 @@ -188,15 +188,15 @@
    15.4  qed "starfunNat2_n_starfunNat2";
    15.5  
    15.6  Goalw [congruent_def] 
    15.7 -      "congruent hypnatrel (%X. hypnatrel^^{%n. f (X n)})";
    15.8 +      "congruent hypnatrel (%X. hypnatrel```{%n. f (X n)})";
    15.9  by (safe_tac (claset()));
   15.10  by (ALLGOALS(Fuf_tac));
   15.11  qed "starfunNat_congruent";
   15.12  
   15.13  (* f::nat=>real *)
   15.14  Goalw [starfunNat_def]
   15.15 -      "(*fNat* f) (Abs_hypnat(hypnatrel^^{%n. X n})) = \
   15.16 -\      Abs_hypreal(hyprel ^^ {%n. f (X n)})";
   15.17 +      "(*fNat* f) (Abs_hypnat(hypnatrel```{%n. X n})) = \
   15.18 +\      Abs_hypreal(hyprel ``` {%n. f (X n)})";
   15.19  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   15.20  by (simp_tac (simpset() addsimps 
   15.21     [hyprel_in_hypreal RS Abs_hypreal_inverse]) 1);
   15.22 @@ -205,8 +205,8 @@
   15.23  
   15.24  (* f::nat=>nat *)
   15.25  Goalw [starfunNat2_def]
   15.26 -      "(*fNat2* f) (Abs_hypnat(hypnatrel^^{%n. X n})) = \
   15.27 -\      Abs_hypnat(hypnatrel ^^ {%n. f (X n)})";
   15.28 +      "(*fNat2* f) (Abs_hypnat(hypnatrel```{%n. X n})) = \
   15.29 +\      Abs_hypnat(hypnatrel ``` {%n. f (X n)})";
   15.30  by (res_inst_tac [("f","Abs_hypnat")] arg_cong 1);
   15.31  by (simp_tac (simpset() addsimps 
   15.32     [hypnatrel_in_hypnat RS Abs_hypnat_inverse,
   15.33 @@ -413,14 +413,14 @@
   15.34       Internal functions - some redundancy with *fNat* now
   15.35   ---------------------------------------------------------*)
   15.36  Goalw [congruent_def] 
   15.37 -      "congruent hypnatrel (%X. hypnatrel^^{%n. f n (X n)})";
   15.38 +      "congruent hypnatrel (%X. hypnatrel```{%n. f n (X n)})";
   15.39  by (safe_tac (claset()));
   15.40  by (ALLGOALS(Fuf_tac));
   15.41  qed "starfunNat_n_congruent";
   15.42  
   15.43  Goalw [starfunNat_n_def]
   15.44 -     "(*fNatn* f) (Abs_hypnat(hypnatrel^^{%n. X n})) = \
   15.45 -\     Abs_hypreal(hyprel ^^ {%n. f n (X n)})";
   15.46 +     "(*fNatn* f) (Abs_hypnat(hypnatrel```{%n. X n})) = \
   15.47 +\     Abs_hypreal(hyprel ``` {%n. f n (X n)})";
   15.48  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   15.49  by Auto_tac;
   15.50  by (Ultra_tac 1);
   15.51 @@ -468,7 +468,7 @@
   15.52  by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus]));
   15.53  qed "starfunNat_n_minus";
   15.54  
   15.55 -Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel ^^ {%i. f i n})";
   15.56 +Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel ``` {%i. f i n})";
   15.57  by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def]));
   15.58  qed "starfunNat_n_eq";
   15.59  Addsimps [starfunNat_n_eq];
    16.1 --- a/src/HOL/Hyperreal/NatStar.thy	Fri Jan 05 18:33:47 2001 +0100
    16.2 +++ b/src/HOL/Hyperreal/NatStar.thy	Fri Jan 05 18:48:18 2001 +0100
    16.3 @@ -23,10 +23,10 @@
    16.4      (* star transform of functions f:Nat --> Real *)
    16.5  
    16.6      starfunNat :: (nat => real) => hypnat => hypreal        ("*fNat* _" [80] 80)
    16.7 -    "*fNat* f  == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel^^{%n. f (X n)}))" 
    16.8 +    "*fNat* f  == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel```{%n. f (X n)}))" 
    16.9  
   16.10      starfunNat_n :: (nat => (nat => real)) => hypnat => hypreal        ("*fNatn* _" [80] 80)
   16.11 -    "*fNatn* F  == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel^^{%n. (F n)(X n)}))" 
   16.12 +    "*fNatn* F  == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel```{%n. (F n)(X n)}))" 
   16.13  
   16.14      InternalNatFuns :: (hypnat => hypreal) set
   16.15      "InternalNatFuns == {X. EX F. X = *fNatn* F}"
   16.16 @@ -34,10 +34,10 @@
   16.17      (* star transform of functions f:Nat --> Nat *)
   16.18  
   16.19      starfunNat2 :: (nat => nat) => hypnat => hypnat        ("*fNat2* _" [80] 80)
   16.20 -    "*fNat2* f  == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel^^{%n. f (X n)}))" 
   16.21 +    "*fNat2* f  == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel```{%n. f (X n)}))" 
   16.22  
   16.23      starfunNat2_n :: (nat => (nat => nat)) => hypnat => hypnat        ("*fNat2n* _" [80] 80)
   16.24 -    "*fNat2n* F  == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel^^{%n. (F n)(X n)}))" 
   16.25 +    "*fNat2n* F  == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel```{%n. (F n)(X n)}))" 
   16.26  
   16.27      InternalNatFuns2 :: (hypnat => hypnat) set
   16.28      "InternalNatFuns2 == {X. EX F. X = *fNat2n* F}"
    17.1 --- a/src/HOL/Hyperreal/SEQ.ML	Fri Jan 05 18:33:47 2001 +0100
    17.2 +++ b/src/HOL/Hyperreal/SEQ.ML	Fri Jan 05 18:48:18 2001 +0100
    17.3 @@ -141,7 +141,7 @@
    17.4  
    17.5  (* thus, the sequence defines an infinite hypernatural! *)
    17.6  Goal "ALL n. n <= f n \
    17.7 -\         ==> Abs_hypnat (hypnatrel ^^ {f}) : HNatInfinite";
    17.8 +\         ==> Abs_hypnat (hypnatrel ``` {f}) : HNatInfinite";
    17.9  by (auto_tac (claset(),simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
   17.10  by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
   17.11  by (etac FreeUltrafilterNat_NSLIMSEQ 1);
   17.12 @@ -156,7 +156,7 @@
   17.13  val lemmaLIM2 = result();
   17.14  
   17.15  Goal "[| #0 < r; ALL n. r <= abs (X (f n) + - L); \
   17.16 -\          (*fNat* X) (Abs_hypnat (hypnatrel ^^ {f})) + \
   17.17 +\          (*fNat* X) (Abs_hypnat (hypnatrel ``` {f})) + \
   17.18  \          - hypreal_of_real  L @= 0 |] ==> False";
   17.19  by (auto_tac (claset(),simpset() addsimps [starfunNat,
   17.20      mem_infmal_iff RS sym,hypreal_of_real_def,
   17.21 @@ -178,7 +178,7 @@
   17.22  by (Step_tac 1);
   17.23  (* skolemization step *)
   17.24  by (dtac choice 1 THEN Step_tac 1);
   17.25 -by (dres_inst_tac [("x","Abs_hypnat(hypnatrel^^{f})")] bspec 1);
   17.26 +by (dres_inst_tac [("x","Abs_hypnat(hypnatrel```{f})")] bspec 1);
   17.27  by (dtac (inf_close_minus_iff RS iffD1) 2);
   17.28  by (fold_tac [real_le_def]);
   17.29  by (blast_tac (claset() addIs [HNatInfinite_NSLIMSEQ]) 1);
   17.30 @@ -511,7 +511,7 @@
   17.31  val lemmaNSBseq2 = result();
   17.32  
   17.33  Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \
   17.34 -\         ==>  Abs_hypreal(hyprel^^{X o f}) : HInfinite";
   17.35 +\         ==>  Abs_hypreal(hyprel```{X o f}) : HInfinite";
   17.36  by (auto_tac (claset(),
   17.37                simpset() addsimps [HInfinite_FreeUltrafilterNat_iff,o_def]));
   17.38  by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
   17.39 @@ -542,7 +542,7 @@
   17.40  val lemma_finite_NSBseq2 = result();
   17.41  
   17.42  Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \
   17.43 -\     ==> Abs_hypnat(hypnatrel^^{f}) : HNatInfinite";
   17.44 +\     ==> Abs_hypnat(hypnatrel```{f}) : HNatInfinite";
   17.45  by (auto_tac (claset(),
   17.46                simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
   17.47  by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
   17.48 @@ -795,7 +795,7 @@
   17.49  (*-------------------------------
   17.50        Standard def => NS def
   17.51   -------------------------------*)
   17.52 -Goal "Abs_hypnat (hypnatrel ^^ {x}) : HNatInfinite \
   17.53 +Goal "Abs_hypnat (hypnatrel ``` {x}) : HNatInfinite \
   17.54  \         ==> {n. M <= x n} : FreeUltrafilterNat";
   17.55  by (auto_tac (claset(),
   17.56                simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
   17.57 @@ -843,7 +843,7 @@
   17.58      step_tac (claset() addSDs [all_conj_distrib RS iffD1]) 1);
   17.59  by (REPEAT(dtac HNatInfinite_NSLIMSEQ 1));
   17.60  by (dtac bspec 1 THEN assume_tac 1);
   17.61 -by (dres_inst_tac [("x","Abs_hypnat (hypnatrel ^^ {fa})")] bspec 1 
   17.62 +by (dres_inst_tac [("x","Abs_hypnat (hypnatrel ``` {fa})")] bspec 1 
   17.63      THEN auto_tac (claset(), simpset() addsimps [starfunNat]));
   17.64  by (dtac (inf_close_minus_iff RS iffD1) 1);
   17.65  by (dtac (mem_infmal_iff RS iffD2) 1);
   17.66 @@ -1334,7 +1334,7 @@
   17.67                   Hyperreals and Sequences
   17.68   ---------------------------------------------------------------***)
   17.69  (*** A bounded sequence is a finite hyperreal ***)
   17.70 -Goal "NSBseq X ==> Abs_hypreal(hyprel^^{X}) : HFinite";
   17.71 +Goal "NSBseq X ==> Abs_hypreal(hyprel```{X}) : HFinite";
   17.72  by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl] addIs 
   17.73         [FreeUltrafilterNat_all RS FreeUltrafilterNat_subset],
   17.74         simpset() addsimps [HFinite_FreeUltrafilterNat_iff,
   17.75 @@ -1343,7 +1343,7 @@
   17.76  
   17.77  (*** A sequence converging to zero defines an infinitesimal ***)
   17.78  Goalw [NSLIMSEQ_def] 
   17.79 -      "X ----NS> #0 ==> Abs_hypreal(hyprel^^{X}) : Infinitesimal";
   17.80 +      "X ----NS> #0 ==> Abs_hypreal(hyprel```{X}) : Infinitesimal";
   17.81  by (dres_inst_tac [("x","whn")] bspec 1);
   17.82  by (simp_tac (simpset() addsimps [HNatInfinite_whn]) 1);
   17.83  by (auto_tac (claset(),
    18.1 --- a/src/HOL/Hyperreal/Star.ML	Fri Jan 05 18:33:47 2001 +0100
    18.2 +++ b/src/HOL/Hyperreal/Star.ML	Fri Jan 05 18:48:18 2001 +0100
    18.3 @@ -108,7 +108,7 @@
    18.4  
    18.5  Goalw [starset_def]
    18.6      "ALL n. (X n) ~: M \
    18.7 -\         ==> Abs_hypreal(hyprel^^{X}) ~: *s* M";
    18.8 +\         ==> Abs_hypreal(hyprel```{X}) ~: *s* M";
    18.9  by (Auto_tac THEN rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   18.10  by (Auto_tac);
   18.11  qed "STAR_real_seq_to_hypreal";
   18.12 @@ -193,14 +193,14 @@
   18.13      Nonstandard extension of functions- congruence 
   18.14   -----------------------------------------------------------------------*) 
   18.15  
   18.16 -Goalw [congruent_def] "congruent hyprel (%X. hyprel^^{%n. f (X n)})";
   18.17 +Goalw [congruent_def] "congruent hyprel (%X. hyprel```{%n. f (X n)})";
   18.18  by (safe_tac (claset()));
   18.19  by (ALLGOALS(Fuf_tac));
   18.20  qed "starfun_congruent";
   18.21  
   18.22  Goalw [starfun_def]
   18.23 -      "(*f* f) (Abs_hypreal(hyprel^^{%n. X n})) = \
   18.24 -\      Abs_hypreal(hyprel ^^ {%n. f (X n)})";
   18.25 +      "(*f* f) (Abs_hypreal(hyprel```{%n. X n})) = \
   18.26 +\      Abs_hypreal(hyprel ``` {%n. f (X n)})";
   18.27  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   18.28  by (simp_tac (simpset() addsimps 
   18.29     [hyprel_in_hypreal RS Abs_hypreal_inverse,[equiv_hyprel,
   18.30 @@ -417,8 +417,8 @@
   18.31     applied entrywise to equivalence class representative.
   18.32     This is easily proved using starfun and ns extension thm
   18.33   ------------------------------------------------------------*)
   18.34 -Goal "abs (Abs_hypreal (hyprel ^^ {X})) = \
   18.35 -\                 Abs_hypreal(hyprel ^^ {%n. abs (X n)})";
   18.36 +Goal "abs (Abs_hypreal (hyprel ``` {X})) = \
   18.37 +\                 Abs_hypreal(hyprel ``` {%n. abs (X n)})";
   18.38  by (simp_tac (simpset() addsimps [starfun_rabs_hrabs RS sym,starfun]) 1);
   18.39  qed "hypreal_hrabs";
   18.40  
   18.41 @@ -470,7 +470,7 @@
   18.42  by (Fuf_tac 1);
   18.43  qed  "Infinitesimal_FreeUltrafilterNat_iff2";
   18.44  
   18.45 -Goal "(Abs_hypreal(hyprel^^{X}) @= Abs_hypreal(hyprel^^{Y})) = \
   18.46 +Goal "(Abs_hypreal(hyprel```{X}) @= Abs_hypreal(hyprel```{Y})) = \
   18.47  \     (ALL m. {n. abs (X n + - Y n) < \
   18.48  \                 inverse(real_of_nat(Suc m))} : FreeUltrafilterNat)";
   18.49  by (rtac (inf_close_minus_iff RS ssubst) 1);
   18.50 @@ -485,6 +485,6 @@
   18.51  Goal "inj starfun";
   18.52  by (rtac injI 1);
   18.53  by (rtac ext 1 THEN rtac ccontr 1);
   18.54 -by (dres_inst_tac [("x","Abs_hypreal(hyprel ^^{%n. xa})")] fun_cong 1);
   18.55 +by (dres_inst_tac [("x","Abs_hypreal(hyprel ```{%n. xa})")] fun_cong 1);
   18.56  by (auto_tac (claset(),simpset() addsimps [starfun]));
   18.57  qed "inj_starfun";
    19.1 --- a/src/HOL/Hyperreal/Star.thy	Fri Jan 05 18:33:47 2001 +0100
    19.2 +++ b/src/HOL/Hyperreal/Star.thy	Fri Jan 05 18:48:18 2001 +0100
    19.3 @@ -25,11 +25,11 @@
    19.4                          ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
    19.5      
    19.6      starfun :: (real => real) => hypreal => hypreal        ("*f* _" [80] 80)
    19.7 -    "*f* f  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel^^{%n. f (X n)}))" 
    19.8 +    "*f* f  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel```{%n. f(X n)}))" 
    19.9  
   19.10      (* internal functions *)
   19.11      starfun_n :: (nat => (real => real)) => hypreal => hypreal        ("*fn* _" [80] 80)
   19.12 -    "*fn* F  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel^^{%n. (F n)(X n)}))" 
   19.13 +    "*fn* F  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel```{%n. (F n)(X n)}))" 
   19.14  
   19.15      InternalFuns :: (hypreal => hypreal) set
   19.16      "InternalFuns == {X. EX F. X = *fn* F}"
    20.1 --- a/src/HOL/Induct/Com.ML	Fri Jan 05 18:33:47 2001 +0100
    20.2 +++ b/src/HOL/Induct/Com.ML	Fri Jan 05 18:48:18 2001 +0100
    20.3 @@ -30,15 +30,15 @@
    20.4  Unify.search_bound := 60;
    20.5  
    20.6  (*Command execution is functional (deterministic) provided evaluation is*)
    20.7 -Goal "univalent ev ==> univalent(exec ev)";
    20.8 -by (simp_tac (simpset() addsimps [univalent_def]) 1);
    20.9 +Goal "single_valued ev ==> single_valued(exec ev)";
   20.10 +by (simp_tac (simpset() addsimps [single_valued_def]) 1);
   20.11  by (REPEAT (rtac allI 1));
   20.12  by (rtac impI 1);
   20.13  by (etac exec.induct 1);
   20.14  by (Blast_tac 3);
   20.15  by (Blast_tac 1);
   20.16 -by (rewrite_goals_tac [univalent_def]);
   20.17 +by (rewrite_goals_tac [single_valued_def]);
   20.18  by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1));
   20.19 -qed "univalent_exec";
   20.20 +qed "single_valued_exec";
   20.21  
   20.22  Addsimps [fun_upd_same, fun_upd_other];
    21.1 --- a/src/HOL/Induct/Exp.ML	Fri Jan 05 18:33:47 2001 +0100
    21.2 +++ b/src/HOL/Induct/Exp.ML	Fri Jan 05 18:48:18 2001 +0100
    21.3 @@ -84,14 +84,14 @@
    21.4  
    21.5  
    21.6  (*Expression evaluation is functional, or deterministic*)
    21.7 -Goalw [univalent_def] "univalent eval";
    21.8 +Goalw [single_valued_def] "single_valued eval";
    21.9  by (EVERY1[rtac allI, rtac allI, rtac impI]);
   21.10  by (split_all_tac 1);
   21.11  by (etac eval_induct 1);
   21.12  by (dtac com_Unique 4);
   21.13  by (ALLGOALS Full_simp_tac);
   21.14  by (ALLGOALS Blast_tac);
   21.15 -qed "univalent_eval";
   21.16 +qed "single_valued_eval";
   21.17  
   21.18  
   21.19  Goal "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
    22.1 --- a/src/HOL/Integ/Equiv.ML	Fri Jan 05 18:33:47 2001 +0100
    22.2 +++ b/src/HOL/Integ/Equiv.ML	Fri Jan 05 18:48:18 2001 +0100
    22.3 @@ -37,33 +37,33 @@
    22.4  
    22.5  (*Lemma for the next result*)
    22.6  Goalw [equiv_def,trans_def,sym_def]
    22.7 -     "[| equiv A r;  (a,b): r |] ==> r^^{a} <= r^^{b}";
    22.8 +     "[| equiv A r;  (a,b): r |] ==> r```{a} <= r```{b}";
    22.9  by (Blast_tac 1);
   22.10  qed "equiv_class_subset";
   22.11  
   22.12 -Goal "[| equiv A r;  (a,b): r |] ==> r^^{a} = r^^{b}";
   22.13 +Goal "[| equiv A r;  (a,b): r |] ==> r```{a} = r```{b}";
   22.14  by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
   22.15  by (rewrite_goals_tac [equiv_def,sym_def]);
   22.16  by (Blast_tac 1);
   22.17  qed "equiv_class_eq";
   22.18  
   22.19 -Goalw [equiv_def,refl_def] "[| equiv A r;  a: A |] ==> a: r^^{a}";
   22.20 +Goalw [equiv_def,refl_def] "[| equiv A r;  a: A |] ==> a: r```{a}";
   22.21  by (Blast_tac 1);
   22.22  qed "equiv_class_self";
   22.23  
   22.24  (*Lemma for the next result*)
   22.25  Goalw [equiv_def,refl_def]
   22.26 -    "[| equiv A r;  r^^{b} <= r^^{a};  b: A |] ==> (a,b): r";
   22.27 +    "[| equiv A r;  r```{b} <= r```{a};  b: A |] ==> (a,b): r";
   22.28  by (Blast_tac 1);
   22.29  qed "subset_equiv_class";
   22.30  
   22.31 -Goal "[| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> (a,b): r";
   22.32 +Goal "[| r```{a} = r```{b};  equiv A r;  b: A |] ==> (a,b): r";
   22.33  by (REPEAT (ares_tac [equalityD2, subset_equiv_class] 1));
   22.34  qed "eq_equiv_class";
   22.35  
   22.36 -(*thus r^^{a} = r^^{b} as well*)
   22.37 +(*thus r```{a} = r```{b} as well*)
   22.38  Goalw [equiv_def,trans_def,sym_def]
   22.39 -     "[| equiv A r;  x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
   22.40 +     "[| equiv A r;  x: (r```{a} Int r```{b}) |] ==> (a,b): r";
   22.41  by (Blast_tac 1);
   22.42  qed "equiv_class_nondisjoint";
   22.43  
   22.44 @@ -71,12 +71,12 @@
   22.45  by (Blast_tac 1);
   22.46  qed "equiv_type";
   22.47  
   22.48 -Goal "equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
   22.49 +Goal "equiv A r ==> ((x,y): r) = (r```{x} = r```{y} & x:A & y:A)";
   22.50  by (blast_tac (claset() addSIs [equiv_class_eq]
   22.51  	                addDs [eq_equiv_class, equiv_type]) 1);
   22.52  qed "equiv_class_eq_iff";
   22.53  
   22.54 -Goal "[| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
   22.55 +Goal "[| equiv A r;  x: A;  y: A |] ==> (r```{x} = r```{y}) = ((x,y): r)";
   22.56  by (blast_tac (claset() addSIs [equiv_class_eq]
   22.57  	                addDs [eq_equiv_class, equiv_type]) 1);
   22.58  qed "eq_equiv_class_iff";
   22.59 @@ -85,12 +85,12 @@
   22.60  
   22.61  (** Introduction/elimination rules -- needed? **)
   22.62  
   22.63 -Goalw [quotient_def] "x:A ==> r^^{x}: A//r";
   22.64 +Goalw [quotient_def] "x:A ==> r```{x}: A//r";
   22.65  by (Blast_tac 1);
   22.66  qed "quotientI";
   22.67  
   22.68  val [major,minor] = Goalw [quotient_def]
   22.69 -    "[| X:(A//r);  !!x. [| X = r^^{x};  x:A |] ==> P |]  \
   22.70 +    "[| X:(A//r);  !!x. [| X = r```{x};  x:A |] ==> P |]  \
   22.71  \    ==> P";
   22.72  by (resolve_tac [major RS UN_E] 1);
   22.73  by (rtac minor 1);
   22.74 @@ -127,7 +127,7 @@
   22.75  
   22.76  (*Conversion rule*)
   22.77  Goal "[| equiv A r;  congruent r b;  a: A |] \
   22.78 -\     ==> (UN x:r^^{a}. b(x)) = b(a)";
   22.79 +\     ==> (UN x:r```{a}. b(x)) = b(a)";
   22.80  by (rtac (equiv_class_self RS UN_constant_eq) 1 THEN REPEAT (assume_tac 1));
   22.81  by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
   22.82  by (blast_tac (claset() delrules [equalityI]) 1);
   22.83 @@ -171,7 +171,7 @@
   22.84  
   22.85  Goalw [congruent_def]
   22.86      "[| equiv A r;  congruent2 r b;  a: A |] ==> \
   22.87 -\    congruent r (%x1. UN x2:r^^{a}. b x1 x2)";
   22.88 +\    congruent r (%x1. UN x2:r```{a}. b x1 x2)";
   22.89  by (Clarify_tac 1);
   22.90  by (rtac (equiv_type RS subsetD RS SigmaE2) 1 THEN REPEAT (assume_tac 1));
   22.91  by (asm_simp_tac (simpset() addsimps [UN_equiv_class,
   22.92 @@ -181,7 +181,7 @@
   22.93  qed "congruent2_implies_congruent_UN";
   22.94  
   22.95  Goal "[| equiv A r;  congruent2 r b;  a1: A;  a2: A |]  \
   22.96 -\    ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2";
   22.97 +\    ==> (UN x1:r```{a1}. UN x2:r```{a2}. b x1 x2) = b a1 a2";
   22.98  by (asm_simp_tac (simpset() addsimps [UN_equiv_class,
   22.99                                       congruent2_implies_congruent,
  22.100                                       congruent2_implies_congruent_UN]) 1);
    23.1 --- a/src/HOL/Integ/Equiv.thy	Fri Jan 05 18:33:47 2001 +0100
    23.2 +++ b/src/HOL/Integ/Equiv.thy	Fri Jan 05 18:48:18 2001 +0100
    23.3 @@ -12,7 +12,7 @@
    23.4      "equiv A r == refl A r & sym(r) & trans(r)"
    23.5  
    23.6    quotient :: "['a set, ('a*'a) set] => 'a set set"  (infixl "'/'/" 90) 
    23.7 -    "A//r == UN x:A. {r^^{x}}"      (*set of equiv classes*)
    23.8 +    "A//r == UN x:A. {r```{x}}"      (*set of equiv classes*)
    23.9  
   23.10    congruent  :: "[('a*'a) set, 'a=>'b] => bool"
   23.11      "congruent r b  == ALL y z. (y,z):r --> b(y)=b(z)"
    24.1 --- a/src/HOL/Integ/IntDef.ML	Fri Jan 05 18:33:47 2001 +0100
    24.2 +++ b/src/HOL/Integ/IntDef.ML	Fri Jan 05 18:48:18 2001 +0100
    24.3 @@ -23,7 +23,7 @@
    24.4  	  [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
    24.5  
    24.6  Goalw [Integ_def,intrel_def,quotient_def]
    24.7 -     "intrel^^{(x,y)}:Integ";
    24.8 +     "intrel```{(x,y)}:Integ";
    24.9  by (Fast_tac 1);
   24.10  qed "intrel_in_integ";
   24.11  
   24.12 @@ -58,18 +58,18 @@
   24.13  (**** zminus: unary negation on Integ ****)
   24.14  
   24.15  Goalw [congruent_def, intrel_def]
   24.16 -     "congruent intrel (%(x,y). intrel^^{(y,x)})";
   24.17 +     "congruent intrel (%(x,y). intrel```{(y,x)})";
   24.18  by (auto_tac (claset(), simpset() addsimps add_ac));
   24.19  qed "zminus_congruent";
   24.20  
   24.21  Goalw [zminus_def]
   24.22 -      "- Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})";
   24.23 +      "- Abs_Integ(intrel```{(x,y)}) = Abs_Integ(intrel ``` {(y,x)})";
   24.24  by (simp_tac (simpset() addsimps 
   24.25  	      [equiv_intrel RS UN_equiv_class, zminus_congruent]) 1);
   24.26  qed "zminus";
   24.27  
   24.28  (*Every integer can be written in the form Abs_Integ(...) *)
   24.29 -val [prem] = Goal "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
   24.30 +val [prem] = Goal "(!!x y. z = Abs_Integ(intrel```{(x,y)}) ==> P) ==> P";
   24.31  by (res_inst_tac [("x1","z")] 
   24.32      (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
   24.33  by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
   24.34 @@ -114,8 +114,8 @@
   24.35  (**** zadd: addition on Integ ****)
   24.36  
   24.37  Goalw [zadd_def]
   24.38 -  "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \
   24.39 -\  Abs_Integ(intrel^^{(x1+x2, y1+y2)})";
   24.40 +  "Abs_Integ(intrel```{(x1,y1)}) + Abs_Integ(intrel```{(x2,y2)}) = \
   24.41 +\  Abs_Integ(intrel```{(x1+x2, y1+y2)})";
   24.42  by (asm_simp_tac (simpset() addsimps [UN_UN_split_split_eq]) 1);
   24.43  by (stac (equiv_intrel RS UN_equiv_class2) 1);
   24.44  by (auto_tac (claset(), simpset() addsimps [congruent2_def]));
   24.45 @@ -232,7 +232,7 @@
   24.46  (*Congruence property for multiplication*)
   24.47  Goal "congruent2 intrel \
   24.48  \       (%p1 p2. (%(x1,y1). (%(x2,y2).   \
   24.49 -\                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
   24.50 +\                   intrel```{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
   24.51  by (rtac (equiv_intrel RS congruent2_commuteI) 1);
   24.52  by (pair_tac "w" 2);
   24.53  by (ALLGOALS Clarify_tac);
   24.54 @@ -249,8 +249,8 @@
   24.55  qed "zmult_congruent2";
   24.56  
   24.57  Goalw [zmult_def]
   24.58 -   "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) =   \
   24.59 -\   Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
   24.60 +   "Abs_Integ((intrel```{(x1,y1)})) * Abs_Integ((intrel```{(x2,y2)})) =   \
   24.61 +\   Abs_Integ(intrel ``` {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
   24.62  by (asm_simp_tac
   24.63      (simpset() addsimps [UN_UN_split_split_eq, zmult_congruent2,
   24.64  			 equiv_intrel RS UN_equiv_class2]) 1);
    25.1 --- a/src/HOL/Integ/IntDef.thy	Fri Jan 05 18:33:47 2001 +0100
    25.2 +++ b/src/HOL/Integ/IntDef.thy	Fri Jan 05 18:48:18 2001 +0100
    25.3 @@ -19,12 +19,12 @@
    25.4  
    25.5  defs
    25.6    zminus_def
    25.7 -    "- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel^^{(y,x)})"
    25.8 +    "- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel```{(y,x)})"
    25.9  
   25.10  constdefs
   25.11  
   25.12    int :: nat => int
   25.13 -  "int m == Abs_Integ(intrel ^^ {(m,0)})"
   25.14 +  "int m == Abs_Integ(intrel ``` {(m,0)})"
   25.15  
   25.16    neg   :: int => bool
   25.17    "neg(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
   25.18 @@ -40,7 +40,7 @@
   25.19    zadd_def
   25.20     "z + w == 
   25.21         Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
   25.22 -		 intrel^^{(x1+x2, y1+y2)})"
   25.23 +		 intrel```{(x1+x2, y1+y2)})"
   25.24  
   25.25    zdiff_def "z - (w::int) == z + (-w)"
   25.26  
   25.27 @@ -51,6 +51,6 @@
   25.28    zmult_def
   25.29     "z * w == 
   25.30         Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
   25.31 -		 intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
   25.32 +		 intrel```{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
   25.33  
   25.34  end
    26.1 --- a/src/HOL/Lex/Automata.ML	Fri Jan 05 18:33:47 2001 +0100
    26.2 +++ b/src/HOL/Lex/Automata.ML	Fri Jan 05 18:48:18 2001 +0100
    26.3 @@ -21,7 +21,7 @@
    26.4  (*** Direct equivalence of NAe and DA ***)
    26.5  
    26.6  Goalw [nae2da_def]
    26.7 - "!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = steps A w ^^ Q";
    26.8 + "!Q. (eps A)^* ``` (DA.delta (nae2da A) w Q) = steps A w ``` Q";
    26.9  by (induct_tac "w" 1);
   26.10   by (Simp_tac 1);
   26.11  by (asm_full_simp_tac (simpset() addsimps [step_def]) 1);
   26.12 @@ -29,7 +29,7 @@
   26.13  qed_spec_mp "espclosure_DA_delta_is_steps";
   26.14  
   26.15  Goalw [nae2da_def]
   26.16 - "fin (nae2da A) Q = (? q : (eps A)^* ^^ Q. fin A q)";
   26.17 + "fin (nae2da A) Q = (? q : (eps A)^* ``` Q. fin A q)";
   26.18  by (Simp_tac 1);
   26.19  val lemma = result();
   26.20  
    27.1 --- a/src/HOL/Lex/Automata.thy	Fri Jan 05 18:33:47 2001 +0100
    27.2 +++ b/src/HOL/Lex/Automata.thy	Fri Jan 05 18:48:18 2001 +0100
    27.3 @@ -14,7 +14,7 @@
    27.4  
    27.5   nae2da :: ('a,'s)nae => ('a,'s set)da
    27.6  "nae2da A == ({start A},
    27.7 -              %a Q. Union(next A (Some a) `` ((eps A)^* ^^ Q)),
    27.8 -              %Q. ? p: (eps A)^* ^^ Q. fin A p)"
    27.9 +              %a Q. Union(next A (Some a) `` ((eps A)^* ``` Q)),
   27.10 +              %Q. ? p: (eps A)^* ``` Q. fin A p)"
   27.11  
   27.12  end
    28.1 --- a/src/HOL/Lex/NAe.thy	Fri Jan 05 18:33:47 2001 +0100
    28.2 +++ b/src/HOL/Lex/NAe.thy	Fri Jan 05 18:48:18 2001 +0100
    28.3 @@ -25,7 +25,7 @@
    28.4  (* not really used:
    28.5  consts delta :: "('a,'s)nae => 'a list => 's => 's set"
    28.6  primrec
    28.7 -"delta A [] s = (eps A)^* ^^ {s}"
    28.8 -"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ^^ {s}))"
    28.9 +"delta A [] s = (eps A)^* ``` {s}"
   28.10 +"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ``` {s}))"
   28.11  *)
   28.12  end
    29.1 --- a/src/HOL/MicroJava/BV/JType.thy	Fri Jan 05 18:33:47 2001 +0100
    29.2 +++ b/src/HOL/MicroJava/BV/JType.thy	Fri Jan 05 18:48:18 2001 +0100
    29.3 @@ -151,7 +151,7 @@
    29.4  done 
    29.5  
    29.6  lemma closed_err_types:
    29.7 -  "[| wf_prog wf_mb G; univalent (subcls1 G); acyclic (subcls1 G) |] 
    29.8 +  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] 
    29.9    ==> closed (err (types G)) (lift2 (sup G))"
   29.10    apply (unfold closed_def plussub_def lift2_def sup_def)
   29.11    apply (auto split: err.split)
   29.12 @@ -163,17 +163,17 @@
   29.13  
   29.14  
   29.15  lemma err_semilat_JType_esl_lemma:
   29.16 -  "[| wf_prog wf_mb G; univalent (subcls1 G); acyclic (subcls1 G) |] 
   29.17 +  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] 
   29.18    ==> err_semilat (esl G)"
   29.19  proof -
   29.20    assume wf_prog:   "wf_prog wf_mb G"
   29.21 -  assume univalent: "univalent (subcls1 G)" 
   29.22 +  assume single_valued: "single_valued (subcls1 G)" 
   29.23    assume acyclic:   "acyclic (subcls1 G)"
   29.24    
   29.25    hence "order (subtype G)"
   29.26      by (rule order_widen)
   29.27    moreover
   29.28 -  from wf_prog univalent acyclic
   29.29 +  from wf_prog single_valued acyclic
   29.30    have "closed (err (types G)) (lift2 (sup G))"
   29.31      by (rule closed_err_types)
   29.32    moreover
   29.33 @@ -185,10 +185,10 @@
   29.34        "G \<turnstile> c1 \<preceq>C Object"
   29.35        "G \<turnstile> c2 \<preceq>C Object"
   29.36        by (blast intro: subcls_C_Object)
   29.37 -    with wf_prog univalent
   29.38 +    with wf_prog single_valued
   29.39      obtain u where
   29.40        "is_lub ((subcls1 G)^* ) c1 c2 u"
   29.41 -      by (blast dest: univalent_has_lubs)
   29.42 +      by (blast dest: single_valued_has_lubs)
   29.43      with acyclic
   29.44      have "G \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2"
   29.45        by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
   29.46 @@ -214,10 +214,10 @@
   29.47        "G \<turnstile> c1 \<preceq>C Object"
   29.48        "G \<turnstile> c2 \<preceq>C Object"
   29.49        by (blast intro: subcls_C_Object)
   29.50 -    with wf_prog univalent
   29.51 +    with wf_prog single_valued
   29.52      obtain u where
   29.53        "is_lub ((subcls1 G)^* ) c2 c1 u"
   29.54 -      by (blast dest: univalent_has_lubs)
   29.55 +      by (blast dest: single_valued_has_lubs)
   29.56      with acyclic
   29.57      have "G \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c2 c1"
   29.58        by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
   29.59 @@ -242,10 +242,10 @@
   29.60        "G \<turnstile> c1 \<preceq>C Object"
   29.61        "G \<turnstile> c2 \<preceq>C Object"
   29.62        by (blast intro: subcls_C_Object)
   29.63 -    with wf_prog univalent
   29.64 +    with wf_prog single_valued
   29.65      obtain u where
   29.66        lub: "is_lub ((subcls1 G)^* ) c1 c2 u"
   29.67 -      by (blast dest: univalent_has_lubs)   
   29.68 +      by (blast dest: single_valued_has_lubs)   
   29.69      with acyclic
   29.70      have "some_lub ((subcls1 G)^* ) c1 c2 = u"
   29.71        by (rule some_lub_conv)
   29.72 @@ -281,14 +281,14 @@
   29.73      by (unfold esl_def semilat_def sl_def) auto
   29.74  qed
   29.75  
   29.76 -lemma univalent_subcls1:
   29.77 -  "wf_prog wf_mb G ==> univalent (subcls1 G)"
   29.78 -  by (unfold wf_prog_def unique_def univalent_def subcls1_def) auto
   29.79 +lemma single_valued_subcls1:
   29.80 +  "wf_prog wf_mb G ==> single_valued (subcls1 G)"
   29.81 +  by (unfold wf_prog_def unique_def single_valued_def subcls1_def) auto
   29.82  
   29.83  ML_setup {* bind_thm ("acyclic_subcls1", acyclic_subcls1) *}
   29.84  
   29.85  theorem err_semilat_JType_esl:
   29.86    "wf_prog wf_mb G ==> err_semilat (esl G)"
   29.87 -  by (frule acyclic_subcls1, frule univalent_subcls1, rule err_semilat_JType_esl_lemma)
   29.88 +  by (frule acyclic_subcls1, frule single_valued_subcls1, rule err_semilat_JType_esl_lemma)
   29.89  
   29.90  end
    30.1 --- a/src/HOL/MicroJava/BV/Semilat.thy	Fri Jan 05 18:33:47 2001 +0100
    30.2 +++ b/src/HOL/MicroJava/BV/Semilat.thy	Fri Jan 05 18:48:18 2001 +0100
    30.3 @@ -193,23 +193,23 @@
    30.4  
    30.5  
    30.6  lemma extend_lub:
    30.7 -  "[| univalent r; is_lub (r^* ) x y u; (x',x) : r |] 
    30.8 +  "[| single_valued r; is_lub (r^* ) x y u; (x',x) : r |] 
    30.9    ==> EX v. is_lub (r^* ) x' y v"
   30.10  apply (unfold is_lub_def is_ub_def)
   30.11  apply (case_tac "(y,x) : r^*")
   30.12   apply (case_tac "(y,x') : r^*")
   30.13    apply blast
   30.14   apply (blast intro: r_into_rtrancl elim: converse_rtranclE
   30.15 -               dest: univalentD)
   30.16 +               dest: single_valuedD)
   30.17  apply (rule exI)
   30.18  apply (rule conjI)
   30.19 - apply (blast intro: rtrancl_into_rtrancl2 dest: univalentD)
   30.20 + apply (blast intro: rtrancl_into_rtrancl2 dest: single_valuedD)
   30.21  apply (blast intro: rtrancl_into_rtrancl rtrancl_into_rtrancl2 
   30.22 -             elim: converse_rtranclE dest: univalentD)
   30.23 +             elim: converse_rtranclE dest: single_valuedD)
   30.24  done 
   30.25  
   30.26 -lemma univalent_has_lubs [rule_format]:
   30.27 -  "[| univalent r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> 
   30.28 +lemma single_valued_has_lubs [rule_format]:
   30.29 +  "[| single_valued r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> 
   30.30    (EX z. is_lub (r^* ) x y z))"
   30.31  apply (erule converse_rtrancl_induct)
   30.32   apply clarify
   30.33 @@ -228,8 +228,8 @@
   30.34  done 
   30.35  
   30.36  lemma is_lub_some_lub:
   30.37 -  "[| univalent r; acyclic r; (x,u):r^*; (y,u):r^* |] 
   30.38 +  "[| single_valued r; acyclic r; (x,u):r^*; (y,u):r^* |] 
   30.39    ==> is_lub (r^* ) x y (some_lub (r^* ) x y)";
   30.40 -  by (fastsimp dest: univalent_has_lubs simp add: some_lub_conv)
   30.41 +  by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv)
   30.42  
   30.43  end
    31.1 --- a/src/HOL/Real/PRat.ML	Fri Jan 05 18:33:47 2001 +0100
    31.2 +++ b/src/HOL/Real/PRat.ML	Fri Jan 05 18:48:18 2001 +0100
    31.3 @@ -61,7 +61,7 @@
    31.4  
    31.5  bind_thm ("equiv_ratrel_iff", [equiv_ratrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
    31.6  
    31.7 -Goalw  [prat_def,ratrel_def,quotient_def] "ratrel^^{(x,y)}:prat";
    31.8 +Goalw  [prat_def,ratrel_def,quotient_def] "ratrel```{(x,y)}:prat";
    31.9  by (Blast_tac 1);
   31.10  qed "ratrel_in_prat";
   31.11  
   31.12 @@ -95,7 +95,7 @@
   31.13  qed "inj_prat_of_pnat";
   31.14  
   31.15  val [prem] = Goal
   31.16 -    "(!!x y. z = Abs_prat(ratrel^^{(x,y)}) ==> P) ==> P";
   31.17 +    "(!!x y. z = Abs_prat(ratrel```{(x,y)}) ==> P) ==> P";
   31.18  by (res_inst_tac [("x1","z")] 
   31.19      (rewrite_rule [prat_def] Rep_prat RS quotientE) 1);
   31.20  by (dres_inst_tac [("f","Abs_prat")] arg_cong 1);
   31.21 @@ -106,12 +106,12 @@
   31.22  
   31.23  (**** qinv: inverse on prat ****)
   31.24  
   31.25 -Goalw [congruent_def] "congruent ratrel (%(x,y). ratrel^^{(y,x)})";
   31.26 +Goalw [congruent_def] "congruent ratrel (%(x,y). ratrel```{(y,x)})";
   31.27  by (auto_tac (claset(), simpset() addsimps [pnat_mult_commute]));  
   31.28  qed "qinv_congruent";
   31.29  
   31.30  Goalw [qinv_def]
   31.31 -      "qinv (Abs_prat(ratrel^^{(x,y)})) = Abs_prat(ratrel ^^ {(y,x)})";
   31.32 +      "qinv (Abs_prat(ratrel```{(x,y)})) = Abs_prat(ratrel ``` {(y,x)})";
   31.33  by (simp_tac (simpset() addsimps 
   31.34  	      [equiv_ratrel RS UN_equiv_class, qinv_congruent]) 1);
   31.35  qed "qinv";
   31.36 @@ -145,7 +145,7 @@
   31.37  qed "prat_add_congruent2_lemma";
   31.38  
   31.39  Goal "congruent2 ratrel (%p1 p2.                  \
   31.40 -\        (%(x1,y1). (%(x2,y2). ratrel^^{(x1*y2 + x2*y1, y1*y2)}) p2) p1)";
   31.41 +\        (%(x1,y1). (%(x2,y2). ratrel```{(x1*y2 + x2*y1, y1*y2)}) p2) p1)";
   31.42  by (rtac (equiv_ratrel RS congruent2_commuteI) 1);
   31.43  by (auto_tac (claset() delrules [equalityI],
   31.44                simpset() addsimps [prat_add_congruent2_lemma]));
   31.45 @@ -153,8 +153,8 @@
   31.46  qed "prat_add_congruent2";
   31.47  
   31.48  Goalw [prat_add_def]
   31.49 -   "Abs_prat((ratrel^^{(x1,y1)})) + Abs_prat((ratrel^^{(x2,y2)})) =   \
   31.50 -\   Abs_prat(ratrel ^^ {(x1*y2 + x2*y1, y1*y2)})";
   31.51 +   "Abs_prat((ratrel```{(x1,y1)})) + Abs_prat((ratrel```{(x2,y2)})) =   \
   31.52 +\   Abs_prat(ratrel ``` {(x1*y2 + x2*y1, y1*y2)})";
   31.53  by (simp_tac (simpset() addsimps [UN_UN_split_split_eq, prat_add_congruent2, 
   31.54  				  equiv_ratrel RS UN_equiv_class2]) 1);
   31.55  qed "prat_add";
   31.56 @@ -189,7 +189,7 @@
   31.57  
   31.58  Goalw [congruent2_def]
   31.59      "congruent2 ratrel (%p1 p2.                  \
   31.60 -\         (%(x1,y1). (%(x2,y2). ratrel^^{(x1*x2, y1*y2)}) p2) p1)";
   31.61 +\         (%(x1,y1). (%(x2,y2). ratrel```{(x1*x2, y1*y2)}) p2) p1)";
   31.62  (*Proof via congruent2_commuteI seems longer*)
   31.63  by (Clarify_tac 1);
   31.64  by (asm_simp_tac (simpset() addsimps [pnat_mult_assoc]) 1);
   31.65 @@ -200,8 +200,8 @@
   31.66  qed "pnat_mult_congruent2";
   31.67  
   31.68  Goalw [prat_mult_def]
   31.69 -  "Abs_prat(ratrel^^{(x1,y1)}) * Abs_prat(ratrel^^{(x2,y2)}) = \
   31.70 -\  Abs_prat(ratrel^^{(x1*x2, y1*y2)})";
   31.71 +  "Abs_prat(ratrel```{(x1,y1)}) * Abs_prat(ratrel```{(x2,y2)}) = \
   31.72 +\  Abs_prat(ratrel```{(x1*x2, y1*y2)})";
   31.73  by (asm_simp_tac 
   31.74      (simpset() addsimps [UN_UN_split_split_eq, pnat_mult_congruent2,
   31.75  			 equiv_ratrel RS UN_equiv_class2]) 1);
   31.76 @@ -389,7 +389,7 @@
   31.77  Goal "!(q::prat). EX x. x + x = q";
   31.78  by (rtac allI 1);
   31.79  by (res_inst_tac [("z","q")] eq_Abs_prat 1);
   31.80 -by (res_inst_tac [("x","Abs_prat (ratrel ^^ {(x, y+y)})")] exI 1);
   31.81 +by (res_inst_tac [("x","Abs_prat (ratrel ``` {(x, y+y)})")] exI 1);
   31.82  by (auto_tac (claset(),
   31.83  	      simpset() addsimps 
   31.84                [prat_add,pnat_mult_assoc RS sym,pnat_add_mult_distrib,
   31.85 @@ -398,7 +398,7 @@
   31.86  
   31.87  Goal "EX (x::prat). x + x = q";
   31.88  by (res_inst_tac [("z","q")] eq_Abs_prat 1);
   31.89 -by (res_inst_tac [("x","Abs_prat (ratrel ^^ {(x, y+y)})")] exI 1);
   31.90 +by (res_inst_tac [("x","Abs_prat (ratrel ``` {(x, y+y)})")] exI 1);
   31.91  by (auto_tac (claset(),simpset() addsimps 
   31.92                [prat_add,pnat_mult_assoc RS sym,pnat_add_mult_distrib,
   31.93                 pnat_add_mult_distrib2]));
   31.94 @@ -454,7 +454,7 @@
   31.95  
   31.96  (* lemma for proving $< is linear *)
   31.97  Goalw [prat_def,prat_less_def] 
   31.98 -      "ratrel ^^ {(x, y * ya)} : {p::(pnat*pnat).True}//ratrel";
   31.99 +      "ratrel ``` {(x, y * ya)} : {p::(pnat*pnat).True}//ratrel";
  31.100  by (asm_full_simp_tac (simpset() addsimps [ratrel_def,quotient_def]) 1);
  31.101  by (Blast_tac 1);
  31.102  qed "lemma_prat_less_linear";
  31.103 @@ -470,15 +470,15 @@
  31.104  by (cut_inst_tac  [("z1.0","x*ya"), ("z2.0","xa*y")] pnat_linear_Ex_eq 1);
  31.105  by (EVERY1[etac disjE,etac exE]);
  31.106  by (eres_inst_tac 
  31.107 -    [("x","Abs_prat(ratrel^^{(xb,ya*y)})")] allE 1);
  31.108 +    [("x","Abs_prat(ratrel```{(xb,ya*y)})")] allE 1);
  31.109  by (asm_full_simp_tac 
  31.110      (simpset() addsimps [prat_add, pnat_mult_assoc 
  31.111       RS sym,pnat_add_mult_distrib RS sym]) 1);
  31.112  by (EVERY1[asm_full_simp_tac (simpset() addsimps pnat_mult_ac),
  31.113      etac disjE, assume_tac, etac exE]);
  31.114 -by (thin_tac "!T. Abs_prat (ratrel ^^ {(x, y)}) + T ~= \
  31.115 -\     Abs_prat (ratrel ^^ {(xa, ya)})" 1);
  31.116 -by (eres_inst_tac [("x","Abs_prat(ratrel^^{(xb,y*ya)})")] allE 1);
  31.117 +by (thin_tac "!T. Abs_prat (ratrel ``` {(x, y)}) + T ~= \
  31.118 +\     Abs_prat (ratrel ``` {(xa, ya)})" 1);
  31.119 +by (eres_inst_tac [("x","Abs_prat(ratrel```{(xb,y*ya)})")] allE 1);
  31.120  by (asm_full_simp_tac (simpset() addsimps [prat_add,
  31.121        pnat_mult_assoc RS sym,pnat_add_mult_distrib RS sym]) 1);
  31.122  by (asm_full_simp_tac (simpset() addsimps pnat_mult_ac) 1);
  31.123 @@ -696,12 +696,12 @@
  31.124  
  31.125  (*** lemmas required for lemma_gleason9_34 in PReal : w*y > y/z ***)
  31.126  Goalw [prat_of_pnat_def] 
  31.127 -      "Abs_prat(ratrel^^{(x,y)}) = (prat_of_pnat x)*qinv(prat_of_pnat y)";
  31.128 +      "Abs_prat(ratrel```{(x,y)}) = (prat_of_pnat x)*qinv(prat_of_pnat y)";
  31.129  by (auto_tac (claset(),simpset() addsimps [prat_mult,qinv,pnat_mult_1_left,
  31.130      pnat_mult_1]));
  31.131  qed "Abs_prat_mult_qinv";
  31.132  
  31.133 -Goal "Abs_prat(ratrel^^{(x,y)}) <= Abs_prat(ratrel^^{(x,Abs_pnat 1)})";
  31.134 +Goal "Abs_prat(ratrel```{(x,y)}) <= Abs_prat(ratrel```{(x,Abs_pnat 1)})";
  31.135  by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
  31.136  by (rtac prat_mult_left_le2_mono1 1);
  31.137  by (rtac qinv_prat_le 1);
  31.138 @@ -713,7 +713,7 @@
  31.139      pSuc_is_plus_one,pnat_one_def,prat_of_pnat_add]));
  31.140  qed "lemma_Abs_prat_le1";
  31.141  
  31.142 -Goal "Abs_prat(ratrel^^{(x,Abs_pnat 1)}) <= Abs_prat(ratrel^^{(x*y,Abs_pnat 1)})";
  31.143 +Goal "Abs_prat(ratrel```{(x,Abs_pnat 1)}) <= Abs_prat(ratrel```{(x*y,Abs_pnat 1)})";
  31.144  by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
  31.145  by (rtac prat_mult_le2_mono1 1);
  31.146  by (pnat_ind_tac "y" 1);
  31.147 @@ -726,19 +726,19 @@
  31.148  			prat_of_pnat_add,prat_of_pnat_mult]));
  31.149  qed "lemma_Abs_prat_le2";
  31.150  
  31.151 -Goal "Abs_prat(ratrel^^{(x,z)}) <= Abs_prat(ratrel^^{(x*y,Abs_pnat 1)})";
  31.152 +Goal "Abs_prat(ratrel```{(x,z)}) <= Abs_prat(ratrel```{(x*y,Abs_pnat 1)})";
  31.153  by (fast_tac (claset() addIs [prat_le_trans,
  31.154  			      lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1);
  31.155  qed "lemma_Abs_prat_le3";
  31.156  
  31.157 -Goal "Abs_prat(ratrel^^{(x*y,Abs_pnat 1)}) * Abs_prat(ratrel^^{(w,x)}) = \
  31.158 -\         Abs_prat(ratrel^^{(w*y,Abs_pnat 1)})";
  31.159 +Goal "Abs_prat(ratrel```{(x*y,Abs_pnat 1)}) * Abs_prat(ratrel```{(w,x)}) = \
  31.160 +\         Abs_prat(ratrel```{(w*y,Abs_pnat 1)})";
  31.161  by (full_simp_tac (simpset() addsimps [prat_mult,
  31.162      pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac) 1);
  31.163  qed "pre_lemma_gleason9_34";
  31.164  
  31.165 -Goal "Abs_prat(ratrel^^{(y*x,Abs_pnat 1*y)}) = \
  31.166 -\         Abs_prat(ratrel^^{(x,Abs_pnat 1)})";
  31.167 +Goal "Abs_prat(ratrel```{(y*x,Abs_pnat 1*y)}) = \
  31.168 +\         Abs_prat(ratrel```{(x,Abs_pnat 1)})";
  31.169  by (auto_tac (claset(),
  31.170  	      simpset() addsimps [pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac));
  31.171  qed "pre_lemma_gleason9_34b";
    32.1 --- a/src/HOL/Real/PRat.thy	Fri Jan 05 18:33:47 2001 +0100
    32.2 +++ b/src/HOL/Real/PRat.thy	Fri Jan 05 18:48:18 2001 +0100
    32.3 @@ -20,20 +20,20 @@
    32.4  constdefs
    32.5  
    32.6    prat_of_pnat :: pnat => prat           
    32.7 -  "prat_of_pnat m == Abs_prat(ratrel^^{(m,Abs_pnat 1)})"
    32.8 +  "prat_of_pnat m == Abs_prat(ratrel```{(m,Abs_pnat 1)})"
    32.9  
   32.10    qinv      :: prat => prat
   32.11 -  "qinv(Q)  == Abs_prat(UN (x,y):Rep_prat(Q). ratrel^^{(y,x)})" 
   32.12 +  "qinv(Q)  == Abs_prat(UN (x,y):Rep_prat(Q). ratrel```{(y,x)})" 
   32.13  
   32.14  defs
   32.15  
   32.16    prat_add_def  
   32.17    "P + Q == Abs_prat(UN (x1,y1):Rep_prat(P). UN (x2,y2):Rep_prat(Q).
   32.18 -		     ratrel^^{(x1*y2 + x2*y1, y1*y2)})"
   32.19 +		     ratrel```{(x1*y2 + x2*y1, y1*y2)})"
   32.20  
   32.21    prat_mult_def  
   32.22    "P * Q == Abs_prat(UN (x1,y1):Rep_prat(P). UN (x2,y2):Rep_prat(Q).
   32.23 -		     ratrel^^{(x1*x2, y1*y2)})"
   32.24 +		     ratrel```{(x1*x2, y1*y2)})"
   32.25   
   32.26    (*** Gleason p. 119 ***)
   32.27    prat_less_def
    33.1 --- a/src/HOL/Real/PReal.ML	Fri Jan 05 18:33:47 2001 +0100
    33.2 +++ b/src/HOL/Real/PReal.ML	Fri Jan 05 18:48:18 2001 +0100
    33.3 @@ -582,10 +582,10 @@
    33.4     prat_of_pnat_add,prat_add_assoc RS sym]));
    33.5  qed "lemma1_gleason9_34";
    33.6  
    33.7 -Goal "Abs_prat (ratrel ^^ {(y, z)}) < xb + \
    33.8 -\         Abs_prat (ratrel ^^ {(x*y, Abs_pnat 1)})*Abs_prat (ratrel ^^ {(w, x)})";
    33.9 -by (res_inst_tac [("j","Abs_prat (ratrel ^^ {(x * y, Abs_pnat 1)}) *\
   33.10 -\                   Abs_prat (ratrel ^^ {(w, x)})")] prat_le_less_trans 1);
   33.11 +Goal "Abs_prat (ratrel ``` {(y, z)}) < xb + \
   33.12 +\         Abs_prat (ratrel ``` {(x*y, Abs_pnat 1)})*Abs_prat (ratrel ``` {(w, x)})";
   33.13 +by (res_inst_tac [("j","Abs_prat (ratrel ``` {(x * y, Abs_pnat 1)}) *\
   33.14 +\                   Abs_prat (ratrel ``` {(w, x)})")] prat_le_less_trans 1);
   33.15  by (rtac prat_self_less_add_right 2);
   33.16  by (auto_tac (claset() addIs [lemma_Abs_prat_le3],
   33.17      simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc]));
    34.1 --- a/src/HOL/Real/RealDef.ML	Fri Jan 05 18:33:47 2001 +0100
    34.2 +++ b/src/HOL/Real/RealDef.ML	Fri Jan 05 18:48:18 2001 +0100
    34.3 @@ -57,11 +57,11 @@
    34.4                         addSEs [sym, preal_trans_lemma]) 1);
    34.5  qed "equiv_realrel";
    34.6  
    34.7 -(* (realrel ^^ {x} = realrel ^^ {y}) = ((x,y) : realrel) *)
    34.8 +(* (realrel ``` {x} = realrel ``` {y}) = ((x,y) : realrel) *)
    34.9  bind_thm ("equiv_realrel_iff",
   34.10      	  [equiv_realrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
   34.11  
   34.12 -Goalw  [real_def,realrel_def,quotient_def] "realrel^^{(x,y)}:real";
   34.13 +Goalw  [real_def,realrel_def,quotient_def] "realrel```{(x,y)}:real";
   34.14  by (Blast_tac 1);
   34.15  qed "realrel_in_real";
   34.16  
   34.17 @@ -95,7 +95,7 @@
   34.18  qed "inj_real_of_preal";
   34.19  
   34.20  val [prem] = Goal
   34.21 -    "(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P";
   34.22 +    "(!!x y. z = Abs_real(realrel```{(x,y)}) ==> P) ==> P";
   34.23  by (res_inst_tac [("x1","z")] 
   34.24      (rewrite_rule [real_def] Rep_real RS quotientE) 1);
   34.25  by (dres_inst_tac [("f","Abs_real")] arg_cong 1);
   34.26 @@ -107,13 +107,13 @@
   34.27  (**** real_minus: additive inverse on real ****)
   34.28  
   34.29  Goalw [congruent_def]
   34.30 -  "congruent realrel (%p. (%(x,y). realrel^^{(y,x)}) p)";
   34.31 +  "congruent realrel (%p. (%(x,y). realrel```{(y,x)}) p)";
   34.32  by (Clarify_tac 1); 
   34.33  by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
   34.34  qed "real_minus_congruent";
   34.35  
   34.36  Goalw [real_minus_def]
   34.37 -      "- (Abs_real(realrel^^{(x,y)})) = Abs_real(realrel ^^ {(y,x)})";
   34.38 +      "- (Abs_real(realrel```{(x,y)})) = Abs_real(realrel ``` {(y,x)})";
   34.39  by (res_inst_tac [("f","Abs_real")] arg_cong 1);
   34.40  by (simp_tac (simpset() addsimps 
   34.41     [realrel_in_real RS Abs_real_inverse,
   34.42 @@ -150,7 +150,7 @@
   34.43  (*** Congruence property for addition ***)
   34.44  Goalw [congruent2_def]
   34.45      "congruent2 realrel (%p1 p2.                  \
   34.46 -\         (%(x1,y1). (%(x2,y2). realrel^^{(x1+x2, y1+y2)}) p2) p1)";
   34.47 +\         (%(x1,y1). (%(x2,y2). realrel```{(x1+x2, y1+y2)}) p2) p1)";
   34.48  by (Clarify_tac 1); 
   34.49  by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1);
   34.50  by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1);
   34.51 @@ -159,8 +159,8 @@
   34.52  qed "real_add_congruent2";
   34.53  
   34.54  Goalw [real_add_def]
   34.55 -  "Abs_real(realrel^^{(x1,y1)}) + Abs_real(realrel^^{(x2,y2)}) = \
   34.56 -\  Abs_real(realrel^^{(x1+x2, y1+y2)})";
   34.57 +  "Abs_real(realrel```{(x1,y1)}) + Abs_real(realrel```{(x2,y2)}) = \
   34.58 +\  Abs_real(realrel```{(x1+x2, y1+y2)})";
   34.59  by (simp_tac (simpset() addsimps 
   34.60                [[equiv_realrel, real_add_congruent2] MRS UN_equiv_class2]) 1);
   34.61  qed "real_add";
   34.62 @@ -301,7 +301,7 @@
   34.63  
   34.64  Goal 
   34.65      "congruent2 realrel (%p1 p2.                  \
   34.66 -\         (%(x1,y1). (%(x2,y2). realrel^^{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)";
   34.67 +\         (%(x1,y1). (%(x2,y2). realrel```{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)";
   34.68  by (rtac (equiv_realrel RS congruent2_commuteI) 1);
   34.69  by (Clarify_tac 1); 
   34.70  by (rewtac split_def);
   34.71 @@ -310,8 +310,8 @@
   34.72  qed "real_mult_congruent2";
   34.73  
   34.74  Goalw [real_mult_def]
   34.75 -   "Abs_real((realrel^^{(x1,y1)})) * Abs_real((realrel^^{(x2,y2)})) =   \
   34.76 -\   Abs_real(realrel ^^ {(x1*x2+y1*y2,x1*y2+x2*y1)})";
   34.77 +   "Abs_real((realrel```{(x1,y1)})) * Abs_real((realrel```{(x2,y2)})) =   \
   34.78 +\   Abs_real(realrel ``` {(x1*x2+y1*y2,x1*y2+x2*y1)})";
   34.79  by (simp_tac (simpset() addsimps
   34.80                 [[equiv_realrel, real_mult_congruent2] MRS UN_equiv_class2]) 1);
   34.81  qed "real_mult";
   34.82 @@ -451,7 +451,7 @@
   34.83  
   34.84  (*** existence of inverse ***)
   34.85  (** lemma -- alternative definition of 0 **)
   34.86 -Goalw [real_zero_def] "0 = Abs_real (realrel ^^ {(x, x)})";
   34.87 +Goalw [real_zero_def] "0 = Abs_real (realrel ``` {(x, x)})";
   34.88  by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
   34.89  qed "real_zero_iff";
   34.90  
   34.91 @@ -461,10 +461,10 @@
   34.92  by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1);
   34.93  by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   34.94             simpset() addsimps [real_zero_iff RS sym]));
   34.95 -by (res_inst_tac [("x","Abs_real (realrel ^^ \
   34.96 +by (res_inst_tac [("x","Abs_real (realrel ``` \
   34.97  \   {(preal_of_prat(prat_of_pnat 1p),pinv(D)+\
   34.98  \    preal_of_prat(prat_of_pnat 1p))})")] exI 1);
   34.99 -by (res_inst_tac [("x","Abs_real (realrel ^^ \
  34.100 +by (res_inst_tac [("x","Abs_real (realrel ``` \
  34.101  \   {(pinv(D)+preal_of_prat(prat_of_pnat 1p),\
  34.102  \    preal_of_prat(prat_of_pnat 1p))})")] exI 2);
  34.103  by (auto_tac (claset(),
  34.104 @@ -716,13 +716,13 @@
  34.105  
  34.106  Goalw [real_of_preal_def]
  34.107        "!!(x::preal). y < x ==> \
  34.108 -\      EX m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m";
  34.109 +\      EX m. Abs_real (realrel ``` {(x,y)}) = real_of_preal m";
  34.110  by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
  34.111      simpset() addsimps preal_add_ac));
  34.112  qed "real_of_preal_ExI";
  34.113  
  34.114  Goalw [real_of_preal_def]
  34.115 -      "!!(x::preal). EX m. Abs_real (realrel ^^ {(x,y)}) = \
  34.116 +      "!!(x::preal). EX m. Abs_real (realrel ``` {(x,y)}) = \
  34.117  \                    real_of_preal m ==> y < x";
  34.118  by (auto_tac (claset(),
  34.119  	      simpset() addsimps 
  34.120 @@ -731,7 +731,7 @@
  34.121      [preal_add_assoc RS sym,preal_self_less_add_left]) 1);
  34.122  qed "real_of_preal_ExD";
  34.123  
  34.124 -Goal "(EX m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m) = (y < x)";
  34.125 +Goal "(EX m. Abs_real (realrel ``` {(x,y)}) = real_of_preal m) = (y < x)";
  34.126  by (blast_tac (claset() addSIs [real_of_preal_ExI,real_of_preal_ExD]) 1);
  34.127  qed "real_of_preal_iff";
  34.128  
    35.1 --- a/src/HOL/Real/RealDef.thy	Fri Jan 05 18:33:47 2001 +0100
    35.2 +++ b/src/HOL/Real/RealDef.thy	Fri Jan 05 18:48:18 2001 +0100
    35.3 @@ -31,14 +31,14 @@
    35.4  defs
    35.5  
    35.6    real_zero_def  
    35.7 -  "0 == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
    35.8 +  "0 == Abs_real(realrel```{(preal_of_prat(prat_of_pnat 1p),
    35.9                                  preal_of_prat(prat_of_pnat 1p))})"
   35.10    real_one_def   
   35.11 -  "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + 
   35.12 +  "1r == Abs_real(realrel```{(preal_of_prat(prat_of_pnat 1p) + 
   35.13              preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})"
   35.14  
   35.15    real_minus_def
   35.16 -  "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
   35.17 +  "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel```{(y,x)})"
   35.18  
   35.19    real_diff_def
   35.20    "R - (S::real) == R + - S"
   35.21 @@ -53,7 +53,7 @@
   35.22  
   35.23    real_of_preal :: preal => real            
   35.24    "real_of_preal m     ==
   35.25 -           Abs_real(realrel^^{(m+preal_of_prat(prat_of_pnat 1p),
   35.26 +           Abs_real(realrel```{(m+preal_of_prat(prat_of_pnat 1p),
   35.27                                 preal_of_prat(prat_of_pnat 1p))})"
   35.28  
   35.29    real_of_posnat :: nat => real             
   35.30 @@ -66,11 +66,11 @@
   35.31  
   35.32    real_add_def  
   35.33    "P+Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
   35.34 -                   (%(x1,y1). (%(x2,y2). realrel^^{(x1+x2, y1+y2)}) p2) p1)"
   35.35 +                   (%(x1,y1). (%(x2,y2). realrel```{(x1+x2, y1+y2)}) p2) p1)"
   35.36    
   35.37    real_mult_def  
   35.38    "P*Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
   35.39 -                   (%(x1,y1). (%(x2,y2). realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)})
   35.40 +                   (%(x1,y1). (%(x2,y2). realrel```{(x1*x2+y1*y2,x1*y2+x2*y1)})
   35.41  		   p2) p1)"
   35.42  
   35.43    real_less_def
    36.1 --- a/src/HOL/Real/RealInt.ML	Fri Jan 05 18:33:47 2001 +0100
    36.2 +++ b/src/HOL/Real/RealInt.ML	Fri Jan 05 18:48:18 2001 +0100
    36.3 @@ -7,7 +7,7 @@
    36.4  
    36.5  
    36.6  Goalw [congruent_def]
    36.7 -  "congruent intrel (%p. (%(i,j). realrel ^^ \
    36.8 +  "congruent intrel (%p. (%(i,j). realrel ``` \
    36.9  \  {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \
   36.10  \    preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)";
   36.11  by (auto_tac (claset(),
   36.12 @@ -16,8 +16,8 @@
   36.13  qed "real_of_int_congruent";
   36.14  
   36.15  Goalw [real_of_int_def]
   36.16 -   "real_of_int (Abs_Integ (intrel ^^ {(i, j)})) = \
   36.17 -\     Abs_real(realrel ^^ \
   36.18 +   "real_of_int (Abs_Integ (intrel ``` {(i, j)})) = \
   36.19 +\     Abs_real(realrel ``` \
   36.20  \       {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \
   36.21  \         preal_of_prat (prat_of_pnat (pnat_of_nat j)))})";
   36.22  by (res_inst_tac [("f","Abs_real")] arg_cong 1);
    37.1 --- a/src/HOL/Real/RealInt.thy	Fri Jan 05 18:33:47 2001 +0100
    37.2 +++ b/src/HOL/Real/RealInt.thy	Fri Jan 05 18:48:18 2001 +0100
    37.3 @@ -9,7 +9,7 @@
    37.4  
    37.5  constdefs 
    37.6     real_of_int :: int => real
    37.7 -   "real_of_int z == Abs_real(UN (i,j): Rep_Integ z. realrel ^^ 
    37.8 +   "real_of_int z == Abs_real(UN (i,j): Rep_Integ z. realrel ```
    37.9                       {(preal_of_prat(prat_of_pnat(pnat_of_nat i)),
   37.10                         preal_of_prat(prat_of_pnat(pnat_of_nat j)))})"
   37.11  
    38.1 --- a/src/HOL/Relation.ML	Fri Jan 05 18:33:47 2001 +0100
    38.2 +++ b/src/HOL/Relation.ML	Fri Jan 05 18:48:18 2001 +0100
    38.3 @@ -333,27 +333,27 @@
    38.4  
    38.5  overload_1st_set "Relation.Image";
    38.6  
    38.7 -Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)";
    38.8 +Goalw [Image_def] "b : r```A = (? x:A. (x,b):r)";
    38.9  by (Blast_tac 1);
   38.10  qed "Image_iff";
   38.11  
   38.12 -Goalw [Image_def] "r^^{a} = {b. (a,b):r}";
   38.13 +Goalw [Image_def] "r```{a} = {b. (a,b):r}";
   38.14  by (Blast_tac 1);
   38.15  qed "Image_singleton";
   38.16  
   38.17 -Goal "(b : r^^{a}) = ((a,b):r)";
   38.18 +Goal "(b : r```{a}) = ((a,b):r)";
   38.19  by (rtac (Image_iff RS trans) 1);
   38.20  by (Blast_tac 1);
   38.21  qed "Image_singleton_iff";
   38.22  
   38.23  AddIffs [Image_singleton_iff];
   38.24  
   38.25 -Goalw [Image_def] "[| (a,b): r;  a:A |] ==> b : r^^A";
   38.26 +Goalw [Image_def] "[| (a,b): r;  a:A |] ==> b : r```A";
   38.27  by (Blast_tac 1);
   38.28  qed "ImageI";
   38.29  
   38.30  val major::prems = Goalw [Image_def]
   38.31 -    "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P";
   38.32 +    "[| b: r```A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P";
   38.33  by (rtac (major RS CollectE) 1);
   38.34  by (Clarify_tac 1);
   38.35  by (rtac (hd prems) 1);
   38.36 @@ -364,72 +364,72 @@
   38.37  AddSEs [ImageE];
   38.38  
   38.39  (*This version's more effective when we already have the required "a"*)
   38.40 -Goal  "[| a:A;  (a,b): r |] ==> b : r^^A";
   38.41 +Goal  "[| a:A;  (a,b): r |] ==> b : r```A";
   38.42  by (Blast_tac 1);
   38.43  qed "rev_ImageI";
   38.44  
   38.45 -Goal "R^^{} = {}";
   38.46 +Goal "R```{} = {}";
   38.47  by (Blast_tac 1);
   38.48  qed "Image_empty";
   38.49  
   38.50  Addsimps [Image_empty];
   38.51  
   38.52 -Goal "Id ^^ A = A";
   38.53 +Goal "Id ``` A = A";
   38.54  by (Blast_tac 1);
   38.55  qed "Image_Id";
   38.56  
   38.57 -Goal "diag A ^^ B = A Int B";
   38.58 +Goal "diag A ``` B = A Int B";
   38.59  by (Blast_tac 1);
   38.60  qed "Image_diag";
   38.61  
   38.62  Addsimps [Image_Id, Image_diag];
   38.63  
   38.64 -Goal "R ^^ (A Int B) <= R ^^ A Int R ^^ B";
   38.65 +Goal "R ``` (A Int B) <= R ``` A Int R ``` B";
   38.66  by (Blast_tac 1);
   38.67  qed "Image_Int_subset";
   38.68  
   38.69 -Goal "R ^^ (A Un B) = R ^^ A Un R ^^ B";
   38.70 +Goal "R ``` (A Un B) = R ``` A Un R ``` B";
   38.71  by (Blast_tac 1);
   38.72  qed "Image_Un";
   38.73  
   38.74 -Goal "r <= A <*> B ==> r^^C <= B";
   38.75 +Goal "r <= A <*> B ==> r```C <= B";
   38.76  by (rtac subsetI 1);
   38.77  by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ;
   38.78  qed "Image_subset";
   38.79  
   38.80  (*NOT suitable for rewriting*)
   38.81 -Goal "r^^B = (UN y: B. r^^{y})";
   38.82 +Goal "r```B = (UN y: B. r```{y})";
   38.83  by (Blast_tac 1);
   38.84  qed "Image_eq_UN";
   38.85  
   38.86 -Goal "[| r'<=r; A'<=A |] ==> (r' ^^ A') <= (r ^^ A)";
   38.87 +Goal "[| r'<=r; A'<=A |] ==> (r' ``` A') <= (r ``` A)";
   38.88  by (Blast_tac 1);
   38.89  qed "Image_mono";
   38.90  
   38.91 -Goal "(r ^^ (UNION A B)) = (UN x:A.(r ^^ (B x)))";
   38.92 +Goal "(r ``` (UNION A B)) = (UN x:A.(r ``` (B x)))";
   38.93  by (Blast_tac 1);
   38.94  qed "Image_UN";
   38.95  
   38.96  (*Converse inclusion fails*)
   38.97 -Goal "(r ^^ (INTER A B)) <= (INT x:A.(r ^^ (B x)))";
   38.98 +Goal "(r ``` (INTER A B)) <= (INT x:A.(r ``` (B x)))";
   38.99  by (Blast_tac 1);
  38.100  qed "Image_INT_subset";
  38.101  
  38.102 -Goal "(r^^A <= B) = (A <= - ((r^-1) ^^ (-B)))";
  38.103 +Goal "(r```A <= B) = (A <= - ((r^-1) ``` (-B)))";
  38.104  by (Blast_tac 1);
  38.105  qed "Image_subset_eq";
  38.106  
  38.107 -section "univalent";
  38.108 +section "single_valued";
  38.109  
  38.110 -Goalw [univalent_def]
  38.111 -     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> univalent r";
  38.112 +Goalw [single_valued_def]
  38.113 +     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> single_valued r";
  38.114  by (assume_tac 1);
  38.115 -qed "univalentI";
  38.116 +qed "single_valuedI";
  38.117  
  38.118 -Goalw [univalent_def]
  38.119 -     "[| univalent r;  (x,y):r;  (x,z):r|] ==> y=z";
  38.120 +Goalw [single_valued_def]
  38.121 +     "[| single_valued r;  (x,y):r;  (x,z):r|] ==> y=z";
  38.122  by Auto_tac;
  38.123 -qed "univalentD";
  38.124 +qed "single_valuedD";
  38.125  
  38.126  
  38.127  (** Graphs given by Collect **)
  38.128 @@ -442,7 +442,7 @@
  38.129  by Auto_tac; 
  38.130  qed "Range_Collect_split";
  38.131  
  38.132 -Goal "{(x,y). P x y} ^^ A = {y. EX x:A. P x y}";
  38.133 +Goal "{(x,y). P x y} ``` A = {y. EX x:A. P x y}";
  38.134  by Auto_tac; 
  38.135  qed "Image_Collect_split";
  38.136  
    39.1 --- a/src/HOL/Relation.thy	Fri Jan 05 18:33:47 2001 +0100
    39.2 +++ b/src/HOL/Relation.thy	Fri Jan 05 18:48:18 2001 +0100
    39.3 @@ -16,8 +16,8 @@
    39.4    comp  :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set"  (infixr "O" 60)
    39.5      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    39.6  
    39.7 -  Image :: "[('a*'b) set,'a set] => 'b set"                (infixl "^^" 90)
    39.8 -    "r ^^ s == {y. ? x:s. (x,y):r}"
    39.9 +  Image :: "[('a*'b) set,'a set] => 'b set"                (infixl "```" 90)
   39.10 +    "r ``` s == {y. ? x:s. (x,y):r}"
   39.11  
   39.12    Id    :: "('a * 'a)set"                            (*the identity relation*)
   39.13      "Id == {p. ? x. p = (x,x)}"
   39.14 @@ -46,8 +46,8 @@
   39.15    trans  :: "('a * 'a)set => bool"          (*transitivity predicate*)
   39.16      "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
   39.17  
   39.18 -  univalent :: "('a * 'b)set => bool"
   39.19 -    "univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
   39.20 +  single_valued :: "('a * 'b)set => bool"
   39.21 +    "single_valued r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
   39.22  
   39.23    fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
   39.24      "fun_rel_comp f R == {g. !x. (f x, g x) : R}"
    40.1 --- a/src/HOL/Relation_Power.ML	Fri Jan 05 18:33:47 2001 +0100
    40.2 +++ b/src/HOL/Relation_Power.ML	Fri Jan 05 18:48:18 2001 +0100
    40.3 @@ -103,12 +103,12 @@
    40.4  qed "rtrancl_is_UN_rel_pow";
    40.5  
    40.6  
    40.7 -Goal "!!r::('a * 'a)set. univalent r ==> univalent (r^n)";
    40.8 -by (rtac univalentI 1);
    40.9 +Goal "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)";
   40.10 +by (rtac single_valuedI 1);
   40.11  by (induct_tac "n" 1);
   40.12   by (Simp_tac 1);
   40.13 -by (fast_tac (claset() addDs [univalentD] addEs [rel_pow_Suc_E]) 1);
   40.14 -qed_spec_mp "univalent_rel_pow";
   40.15 +by (fast_tac (claset() addDs [single_valuedD] addEs [rel_pow_Suc_E]) 1);
   40.16 +qed_spec_mp "single_valued_rel_pow";
   40.17  
   40.18  
   40.19  
    41.1 --- a/src/HOL/UNITY/Extend.ML	Fri Jan 05 18:33:47 2001 +0100
    41.2 +++ b/src/HOL/UNITY/Extend.ML	Fri Jan 05 18:48:18 2001 +0100
    41.3 @@ -58,7 +58,7 @@
    41.4  by (Blast_tac 1);
    41.5  qed "Domain_Restrict";
    41.6  
    41.7 -Goal "(Restrict A r) ^^ B = r ^^ (A Int B)";
    41.8 +Goal "(Restrict A r) ``` B = r ``` (A Int B)";
    41.9  by (Blast_tac 1);
   41.10  qed "Image_Restrict";
   41.11  
   41.12 @@ -308,7 +308,7 @@
   41.13  qed "inj_extend_act";
   41.14  
   41.15  Goalw [extend_set_def, extend_act_def]
   41.16 -     "extend_act h act ^^ (extend_set h A) = extend_set h (act ^^ A)";
   41.17 +     "extend_act h act ``` (extend_set h A) = extend_set h (act ``` A)";
   41.18  by (Force_tac 1);
   41.19  qed "extend_act_Image";
   41.20  Addsimps [extend_act_Image];
    42.1 --- a/src/HOL/UNITY/FP.ML	Fri Jan 05 18:33:47 2001 +0100
    42.2 +++ b/src/HOL/UNITY/FP.ML	Fri Jan 05 18:48:18 2001 +0100
    42.3 @@ -49,11 +49,11 @@
    42.4  qed "FP_weakest";
    42.5  
    42.6  Goalw [FP_def, stable_def, constrains_def]
    42.7 -    "-(FP F) = (UN act: Acts F. -{s. act^^{s} <= {s}})";
    42.8 +    "-(FP F) = (UN act: Acts F. -{s. act```{s} <= {s}})";
    42.9  by (Blast_tac 1);
   42.10  qed "Compl_FP";
   42.11  
   42.12 -Goal "A - (FP F) = (UN act: Acts F. A - {s. act^^{s} <= {s}})";
   42.13 +Goal "A - (FP F) = (UN act: Acts F. A - {s. act```{s} <= {s}})";
   42.14  by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1);
   42.15  qed "Diff_FP";
   42.16  
    43.1 --- a/src/HOL/UNITY/PriorityAux.ML	Fri Jan 05 18:33:47 2001 +0100
    43.2 +++ b/src/HOL/UNITY/PriorityAux.ML	Fri Jan 05 18:48:18 2001 +0100
    43.3 @@ -20,14 +20,14 @@
    43.4  (* The equalities (above i r = {}) = (A i r = {}) 
    43.5     and (reach i r = {}) = (R i r) rely on the following theorem  *)
    43.6  
    43.7 -Goal "((r^+)^^{i} = {}) = (r^^{i} = {})";
    43.8 +Goal "((r^+)```{i} = {}) = (r```{i} = {})";
    43.9  by Auto_tac;
   43.10  by (etac trancl_induct 1);
   43.11  by Auto_tac;
   43.12  qed "image0_trancl_iff_image0_r";
   43.13  
   43.14  (* Another form usefull in some situation *)
   43.15 -Goal "(r^^{i}={}) = (ALL x. ((i,x):r^+) = False)";
   43.16 +Goal "(r```{i}={}) = (ALL x. ((i,x):r^+) = False)";
   43.17  by Auto_tac;
   43.18  by (dtac (image0_trancl_iff_image0_r RS ssubst) 1);
   43.19  by Auto_tac;
   43.20 @@ -76,7 +76,7 @@
   43.21  
   43.22  (* Lemma 2 *)
   43.23  Goal 
   43.24 -"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)^^{z}={})";
   43.25 +"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)```{z}={})";
   43.26  by Auto_tac;
   43.27  by (forw_inst_tac [("r", "r")] trancl_into_trancl2 1);
   43.28  by Auto_tac;
   43.29 @@ -86,7 +86,7 @@
   43.30   "acyclic r ==> A i r~={}-->(EX j:above i r. A j r = {})";
   43.31  by (full_simp_tac (simpset() 
   43.32              addsimps [acyclic_eq_wf, wf_eq_minimal]) 1);
   43.33 -by (dres_inst_tac [("x", "((r^-1)^+)^^{i}")] spec 1);
   43.34 +by (dres_inst_tac [("x", "((r^-1)^+)```{i}")] spec 1);
   43.35  by Auto_tac;
   43.36  by (rotate_tac ~1 1);
   43.37  by (asm_full_simp_tac (simpset() 
    44.1 --- a/src/HOL/UNITY/PriorityAux.thy	Fri Jan 05 18:33:47 2001 +0100
    44.2 +++ b/src/HOL/UNITY/PriorityAux.thy	Fri Jan 05 18:48:18 2001 +0100
    44.3 @@ -18,20 +18,20 @@
    44.4  
    44.5    (* Neighbors of a vertex i *)
    44.6    neighbors :: "[vertex, (vertex*vertex)set]=>vertex set"
    44.7 - "neighbors i r == ((r Un r^-1)^^{i}) - {i}"
    44.8 + "neighbors i r == ((r Un r^-1)```{i}) - {i}"
    44.9  
   44.10    R :: "[vertex, (vertex*vertex)set]=>vertex set"
   44.11 -  "R i r == r^^{i}"
   44.12 +  "R i r == r```{i}"
   44.13  
   44.14    A :: "[vertex, (vertex*vertex)set]=>vertex set"
   44.15 -  "A i r == (r^-1)^^{i}"
   44.16 +  "A i r == (r^-1)```{i}"
   44.17  
   44.18    (* reachable and above vertices: the original notation was R* and A* *)  
   44.19    reach :: "[vertex, (vertex*vertex)set]=> vertex set"
   44.20 -  "reach i r == (r^+)^^{i}"
   44.21 +  "reach i r == (r^+)```{i}"
   44.22  
   44.23    above :: "[vertex, (vertex*vertex)set]=> vertex set"
   44.24 -  "above i r == ((r^-1)^+)^^{i}"  
   44.25 +  "above i r == ((r^-1)^+)```{i}"  
   44.26  
   44.27    reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set"
   44.28    "reverse i r == (r - {(x,y). x=i | y=i} Int r) Un ({(x,y). x=i|y=i} Int r)^-1"
    45.1 --- a/src/HOL/UNITY/Project.ML	Fri Jan 05 18:33:47 2001 +0100
    45.2 +++ b/src/HOL/UNITY/Project.ML	Fri Jan 05 18:48:18 2001 +0100
    45.3 @@ -384,7 +384,7 @@
    45.4       "[| G : transient (C Int extend_set h A);  G : stable C |]  \
    45.5  \     ==> project h C G : transient (project_set h C Int A)";
    45.6  by (auto_tac (claset(), simpset() addsimps [Domain_project_act]));
    45.7 -by (subgoal_tac "act ^^ (C Int extend_set h A) <= - extend_set h A" 1);
    45.8 +by (subgoal_tac "act ``` (C Int extend_set h A) <= - extend_set h A" 1);
    45.9  by (asm_full_simp_tac 
   45.10      (simpset() addsimps [stable_def, constrains_def]) 2);
   45.11  by (Blast_tac 2);
   45.12 @@ -502,8 +502,8 @@
   45.13  
   45.14  
   45.15  Goalw [project_set_def, extend_set_def, project_act_def]
   45.16 -     "act ^^ (C Int extend_set h A) <= B \
   45.17 -\     ==> project_act h (Restrict C act) ^^ (project_set h C Int A) \
   45.18 +     "act ``` (C Int extend_set h A) <= B \
   45.19 +\     ==> project_act h (Restrict C act) ``` (project_set h C Int A) \
   45.20  \         <= project_set h B";
   45.21  by (Blast_tac 1);
   45.22  qed "act_subset_imp_project_act_subset";
   45.23 @@ -512,9 +512,9 @@
   45.24    property upwards.  The hard part would be to 
   45.25    show that G's action has a big enough domain.*)
   45.26  Goal "[| act: Acts G;       \
   45.27 -\        (project_act h (Restrict C act))^^ \
   45.28 +\        (project_act h (Restrict C act))``` \
   45.29  \             (project_set h C Int A - B) <= -(project_set h C Int A - B) |] \
   45.30 -\     ==> act^^(C Int extend_set h A - extend_set h B) \
   45.31 +\     ==> act```(C Int extend_set h A - extend_set h B) \
   45.32  \           <= -(C Int extend_set h A - extend_set h B)"; 
   45.33  by (auto_tac (claset(), 
   45.34       simpset() addsimps [project_set_def, extend_set_def, project_act_def]));  
   45.35 @@ -535,8 +535,8 @@
   45.36  				  extend_set_Diff_distrib RS sym]));
   45.37  by (dtac act_subset_imp_project_act_subset 1);
   45.38  by (subgoal_tac
   45.39 -    "project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) = {}" 1);
   45.40 -by (REPEAT (thin_tac "?r^^?A <= ?B" 1));
   45.41 +    "project_act h (Restrict C act) ``` (project_set h C Int (A - B)) = {}" 1);
   45.42 +by (REPEAT (thin_tac "?r```?A <= ?B" 1));
   45.43  by (rewrite_goals_tac [project_set_def, extend_set_def, project_act_def]);
   45.44  by (Blast_tac 2);
   45.45  by (rtac ccontr 1);
    46.1 --- a/src/HOL/UNITY/SubstAx.ML	Fri Jan 05 18:33:47 2001 +0100
    46.2 +++ b/src/HOL/UNITY/SubstAx.ML	Fri Jan 05 18:48:18 2001 +0100
    46.3 @@ -314,7 +314,7 @@
    46.4  (** Meta or object quantifier ????? **)
    46.5  Goal "[| wf r;     \
    46.6  \        ALL m. F : (A Int f-``{m}) LeadsTo                     \
    46.7 -\                           ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
    46.8 +\                           ((A Int f-``(r^-1 ``` {m})) Un B) |] \
    46.9  \     ==> F : A LeadsTo B";
   46.10  by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1);
   46.11  by (etac leadsTo_wf_induct 1);
   46.12 @@ -324,7 +324,7 @@
   46.13  
   46.14  Goal "[| wf r;     \
   46.15  \        ALL m:I. F : (A Int f-``{m}) LeadsTo                   \
   46.16 -\                             ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
   46.17 +\                             ((A Int f-``(r^-1 ``` {m})) Un B) |] \
   46.18  \     ==> F : A LeadsTo ((A - (f-``I)) Un B)";
   46.19  by (etac LeadsTo_wf_induct 1);
   46.20  by Safe_tac;
    47.1 --- a/src/HOL/UNITY/UNITY.ML	Fri Jan 05 18:33:47 2001 +0100
    47.2 +++ b/src/HOL/UNITY/UNITY.ML	Fri Jan 05 18:48:18 2001 +0100
    47.3 @@ -389,11 +389,11 @@
    47.4  
    47.5  (** Needed for WF reasoning in WFair.ML **)
    47.6  
    47.7 -Goal "less_than ^^ {k} = greaterThan k";
    47.8 +Goal "less_than ``` {k} = greaterThan k";
    47.9  by (Blast_tac 1);
   47.10  qed "Image_less_than";
   47.11  
   47.12 -Goal "less_than^-1 ^^ {k} = lessThan k";
   47.13 +Goal "less_than^-1 ``` {k} = lessThan k";
   47.14  by (Blast_tac 1);
   47.15  qed "Image_inverse_less_than";
   47.16  
    48.1 --- a/src/HOL/UNITY/UNITY.thy	Fri Jan 05 18:33:47 2001 +0100
    48.2 +++ b/src/HOL/UNITY/UNITY.thy	Fri Jan 05 18:48:18 2001 +0100
    48.3 @@ -51,7 +51,7 @@
    48.4  
    48.5  
    48.6  defs
    48.7 -  constrains_def "A co B == {F. ALL act: Acts F. act^^A <= B}"
    48.8 +  constrains_def "A co B == {F. ALL act: Acts F. act```A <= B}"
    48.9  
   48.10    unless_def     "A unless B == (A-B) co (A Un B)"
   48.11  
    49.1 --- a/src/HOL/UNITY/WFair.ML	Fri Jan 05 18:33:47 2001 +0100
    49.2 +++ b/src/HOL/UNITY/WFair.ML	Fri Jan 05 18:48:18 2001 +0100
    49.3 @@ -27,14 +27,14 @@
    49.4  qed "transient_strengthen";
    49.5  
    49.6  Goalw [transient_def]
    49.7 -    "[| act: Acts F;  A <= Domain act;  act^^A <= -A |] ==> F : transient A";
    49.8 +    "[| act: Acts F;  A <= Domain act;  act```A <= -A |] ==> F : transient A";
    49.9  by (Blast_tac 1);
   49.10  qed "transientI";
   49.11  
   49.12  val major::prems = 
   49.13  Goalw [transient_def]
   49.14      "[| F : transient A;  \
   49.15 -\       !!act. [| act: Acts F;  A <= Domain act;  act^^A <= -A |] ==> P |] \
   49.16 +\       !!act. [| act: Acts F;  A <= Domain act;  act```A <= -A |] ==> P |] \
   49.17  \    ==> P";
   49.18  by (rtac (major RS CollectD RS bexE) 1);
   49.19  by (blast_tac (claset() addIs prems) 1);
   49.20 @@ -362,10 +362,10 @@
   49.21  
   49.22  Goal "[| wf r;     \
   49.23  \        ALL m. F : (A Int f-``{m}) leadsTo                     \
   49.24 -\                   ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
   49.25 +\                   ((A Int f-``(r^-1 ``` {m})) Un B) |] \
   49.26  \     ==> F : (A Int f-``{m}) leadsTo B";
   49.27  by (eres_inst_tac [("a","m")] wf_induct 1);
   49.28 -by (subgoal_tac "F : (A Int (f -`` (r^-1 ^^ {x}))) leadsTo B" 1);
   49.29 +by (subgoal_tac "F : (A Int (f -`` (r^-1 ``` {x}))) leadsTo B" 1);
   49.30  by (stac vimage_eq_UN 2);
   49.31  by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2);
   49.32  by (blast_tac (claset() addIs [leadsTo_UN]) 2);
   49.33 @@ -376,7 +376,7 @@
   49.34  (** Meta or object quantifier ? **)
   49.35  Goal "[| wf r;     \
   49.36  \        ALL m. F : (A Int f-``{m}) leadsTo                     \
   49.37 -\                   ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
   49.38 +\                   ((A Int f-``(r^-1 ``` {m})) Un B) |] \
   49.39  \     ==> F : A leadsTo B";
   49.40  by (res_inst_tac [("t", "A")] subst 1);
   49.41  by (rtac leadsTo_UN 2);
   49.42 @@ -388,7 +388,7 @@
   49.43  
   49.44  Goal "[| wf r;     \
   49.45  \        ALL m:I. F : (A Int f-``{m}) leadsTo                   \
   49.46 -\                     ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
   49.47 +\                     ((A Int f-``(r^-1 ``` {m})) Un B) |] \
   49.48  \     ==> F : A leadsTo ((A - (f-``I)) Un B)";
   49.49  by (etac leadsTo_wf_induct 1);
   49.50  by Safe_tac;
    50.1 --- a/src/HOL/UNITY/WFair.thy	Fri Jan 05 18:33:47 2001 +0100
    50.2 +++ b/src/HOL/UNITY/WFair.thy	Fri Jan 05 18:48:18 2001 +0100
    50.3 @@ -15,7 +15,7 @@
    50.4    (*This definition specifies weak fairness.  The rest of the theory
    50.5      is generic to all forms of fairness.*)
    50.6    transient :: "'a set => 'a program set"
    50.7 -    "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
    50.8 +    "transient A == {F. EX act: Acts F. A <= Domain act & act```A <= -A}"
    50.9  
   50.10    ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
   50.11      "A ensures B == (A-B co A Un B) Int transient (A-B)"
    51.1 --- a/src/HOL/ex/Tarski.ML	Fri Jan 05 18:33:47 2001 +0100
    51.2 +++ b/src/HOL/ex/Tarski.ML	Fri Jan 05 18:48:18 2001 +0100
    51.3 @@ -400,7 +400,7 @@
    51.4  by (simp_tac (simpset() addsimps PO_simp) 1);
    51.5  qed "CLF_E2";
    51.6  
    51.7 -Goal "f : CLF ^^ {cl} ==> f : CLF ^^ {dual cl}";
    51.8 +Goal "f : CLF ``` {cl} ==> f : CLF ``` {dual cl}";
    51.9  by (afs [CLF_def, CL_dualCL, monotone_dual] 1); 
   51.10  by (afs [dualA_iff] 1);
   51.11  qed "CLF_dual";
    52.1 --- a/src/HOL/ex/Tarski.thy	Fri Jan 05 18:33:47 2001 +0100
    52.2 +++ b/src/HOL/ex/Tarski.thy	Fri Jan 05 18:48:18 2001 +0100
    52.3 @@ -94,7 +94,7 @@
    52.4    "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
    52.5  
    52.6  translations
    52.7 -  "S <<= cl" == "S : sublattice ^^ {cl}"
    52.8 +  "S <<= cl" == "S : sublattice ``` {cl}"
    52.9  
   52.10  constdefs
   52.11    dual :: "'a potype => 'a potype"
   52.12 @@ -121,7 +121,7 @@
   52.13    f :: "'a => 'a"
   52.14    P :: "'a set"
   52.15  assumes 
   52.16 -  f_cl "f : CLF ^^{cl}"
   52.17 +  f_cl "f : CLF```{cl}"
   52.18  defines
   52.19    P_def "P == fix f A"
   52.20