# 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