1.1 --- a/src/HOL/ex/LocaleTest2.thy	Wed Oct 10 17:31:52 2007 +0200
     1.2 +++ b/src/HOL/ex/LocaleTest2.thy	Wed Oct 10 17:31:53 2007 +0200
     1.3 @@ -472,12 +472,12 @@
     1.4  
     1.5  interpretation int: dpo ["op <= :: [int, int] => bool"]
     1.6    where "(dpo.less (op <=) (x::int) y) = (x < y)"
     1.7 -  txt {* We give interpretation for less, but not is\_inf and is\_sub. *}
     1.8 +  txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
     1.9  proof -
    1.10    show "dpo (op <= :: [int, int] => bool)"
    1.11      by unfold_locales auto
    1.12    then interpret int: dpo ["op <= :: [int, int] => bool"] .
    1.13 -    txt {* Gives interpreted version of less\_def (without condition). *}
    1.14 +    txt {* Gives interpreted version of @{text less_def} (without condition). *}
    1.15    show "(dpo.less (op <=) (x::int) y) = (x < y)"
    1.16      by (unfold int.less_def) auto
    1.17  qed
    1.18 @@ -528,12 +528,12 @@
    1.19  
    1.20  interpretation nat: dpo ["op <= :: [nat, nat] => bool"]
    1.21    where "dpo.less (op <=) (x::nat) y = (x < y)"
    1.22 -  txt {* We give interpretation for less, but not is\_inf and is\_sub. *}
    1.23 +  txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
    1.24  proof -
    1.25    show "dpo (op <= :: [nat, nat] => bool)"
    1.26      by unfold_locales auto
    1.27    then interpret nat: dpo ["op <= :: [nat, nat] => bool"] .
    1.28 -    txt {* Gives interpreted version of less\_def (without condition). *}
    1.29 +    txt {* Gives interpreted version of @{text less_def} (without condition). *}
    1.30    show "dpo.less (op <=) (x::nat) y = (x < y)"
    1.31      apply (unfold nat.less_def)
    1.32      apply auto
    1.33 @@ -579,12 +579,12 @@
    1.34  
    1.35  interpretation nat_dvd: dpo ["op dvd :: [nat, nat] => bool"]
    1.36    where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
    1.37 -  txt {* We give interpretation for less, but not is\_inf and is\_sub. *}
    1.38 +  txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
    1.39  proof -
    1.40    show "dpo (op dvd :: [nat, nat] => bool)"
    1.41      by unfold_locales (auto simp: dvd_def)
    1.42    then interpret nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] .
    1.43 -    txt {* Gives interpreted version of less\_def (without condition). *}
    1.44 +    txt {* Gives interpreted version of @{text less_def} (without condition). *}
    1.45    show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
    1.46      apply (unfold nat_dvd.less_def)
    1.47      apply auto