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/HOLCF/Porder.thy
changeset 69597 ff784d5a5bfb
parent 68780 54fdc8bc73a3 
--- a/src/HOL/HOLCF/Porder.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/HOLCF/Porder.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -149,7 +149,7 @@
 lemma is_lub_unique: "S <<| x \<Longrightarrow> S <<| y \<Longrightarrow> x = y"
   unfolding is_lub_def is_ub_def by (blast intro: below_antisym)
 
-text \<open>technical lemmas about @{term lub} and @{term is_lub}\<close>
+text \<open>technical lemmas about \<^term>\<open>lub\<close> and \<^term>\<open>is_lub\<close>\<close>
 
 lemma is_lub_lub: "M <<| x \<Longrightarrow> M <<| lub M"
   unfolding lub_def by (rule theI [OF _ is_lub_unique])
isabelle