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/UNITY/Extend.thy
changeset 69597 ff784d5a5bfb
parent 69313 b021008c5397 
--- a/src/HOL/UNITY/Extend.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/UNITY/Extend.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -167,7 +167,7 @@
 end
 
 
-subsection\<open>@{term extend_set}: basic properties\<close>
+subsection\<open>\<^term>\<open>extend_set\<close>: basic properties\<close>
 
 lemma project_set_iff [iff]:
      "(x \<in> project_set h C) = (\<exists>y. h(x,y) \<in> C)"
@@ -215,7 +215,7 @@
 apply (auto simp add: split_extended_all)
 done
 
-subsection\<open>@{term project_set}: basic properties\<close>
+subsection\<open>\<^term>\<open>project_set\<close>: basic properties\<close>
 
 (*project_set is simply image!*)
 lemma project_set_eq: "project_set h C = f ` C"
@@ -262,7 +262,7 @@
   by (auto simp: extend_set_def)
 
 
-subsection\<open>@{term extend_act}\<close>
+subsection\<open>\<^term>\<open>extend_act\<close>\<close>
 
 (*Can't strengthen it to
   ((h(s,y), h(s',y')) \<in> extend_act h act) = ((s, s') \<in> act & y=y')
isabelle