# HG changeset patch
# User wenzelm
# Date 1192030313 -7200
# Node ID a7bcad4137998a9ada62c3277b21ad485222896d
# Parent  2c27817065bca63b5776c5d25456a392f46f5575
proper latex antiquotations instead of adhoc escapes;

diff -r 2c27817065bc -r a7bcad413799 src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Wed Oct 10 17:31:52 2007 +0200
+++ b/src/HOL/ex/LocaleTest2.thy	Wed Oct 10 17:31:53 2007 +0200
@@ -472,12 +472,12 @@
 
 interpretation int: dpo ["op <= :: [int, int] => bool"]
   where "(dpo.less (op <=) (x::int) y) = (x < y)"
-  txt {* We give interpretation for less, but not is\_inf and is\_sub. *}
+  txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
   show "dpo (op <= :: [int, int] => bool)"
     by unfold_locales auto
   then interpret int: dpo ["op <= :: [int, int] => bool"] .
-    txt {* Gives interpreted version of less\_def (without condition). *}
+    txt {* Gives interpreted version of @{text less_def} (without condition). *}
   show "(dpo.less (op <=) (x::int) y) = (x < y)"
     by (unfold int.less_def) auto
 qed
@@ -528,12 +528,12 @@
 
 interpretation nat: dpo ["op <= :: [nat, nat] => bool"]
   where "dpo.less (op <=) (x::nat) y = (x < y)"
-  txt {* We give interpretation for less, but not is\_inf and is\_sub. *}
+  txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
   show "dpo (op <= :: [nat, nat] => bool)"
     by unfold_locales auto
   then interpret nat: dpo ["op <= :: [nat, nat] => bool"] .
-    txt {* Gives interpreted version of less\_def (without condition). *}
+    txt {* Gives interpreted version of @{text less_def} (without condition). *}
   show "dpo.less (op <=) (x::nat) y = (x < y)"
     apply (unfold nat.less_def)
     apply auto
@@ -579,12 +579,12 @@
 
 interpretation nat_dvd: dpo ["op dvd :: [nat, nat] => bool"]
   where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
-  txt {* We give interpretation for less, but not is\_inf and is\_sub. *}
+  txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
   show "dpo (op dvd :: [nat, nat] => bool)"
     by unfold_locales (auto simp: dvd_def)
   then interpret nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] .
-    txt {* Gives interpreted version of less\_def (without condition). *}
+    txt {* Gives interpreted version of @{text less_def} (without condition). *}
   show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
     apply (unfold nat_dvd.less_def)
     apply auto