author wenzelm Wed, 10 Oct 2007 17:31:53 +0200 changeset 24946 a7bcad413799 parent 24945 2c27817065bc child 24947 b7e990e1706a
```--- 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```