Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/LocaleTest2.thy
changeset 69597 ff784d5a5bfb
parent 69064 5840724b1d71 
--- a/src/HOL/ex/LocaleTest2.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -466,7 +466,7 @@
   qed
 qed
 
-subsubsection \<open>Total order \<open><=\<close> on @{typ int}\<close>
+subsubsection \<open>Total order \<open><=\<close> on \<^typ>\<open>int\<close>\<close>
 
 interpretation int: dpo "(<=) :: [int, int] => bool"
   rewrites "(dpo.less (<=) (x::int) y) = (x < y)"
@@ -522,7 +522,7 @@
 thm int.less_total text \<open>from dlo\<close>
 
 
-subsubsection \<open>Total order \<open><=\<close> on @{typ nat}\<close>
+subsubsection \<open>Total order \<open><=\<close> on \<^typ>\<open>nat\<close>\<close>
 
 interpretation nat: dpo "(<=) :: [nat, nat] => bool"
   rewrites "dpo.less (<=) (x::nat) y = (x < y)"
@@ -573,7 +573,7 @@
 thm nat.less_total text \<open>from ldo\<close>
 
 
-subsubsection \<open>Lattice \<open>dvd\<close> on @{typ nat}\<close>
+subsubsection \<open>Lattice \<open>dvd\<close> on \<^typ>\<open>nat\<close>\<close>
 
 interpretation nat_dvd: dpo "(dvd) :: [nat, nat] => bool"
   rewrites "dpo.less (dvd) (x::nat) y = (x dvd y & x ~= y)"
isabelle