src/HOL/UNITY/Extend.thy

 qed 
 
 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)"
 by (simp add: project_set_def)
 

 lemma extend_set_UNIV_eq [simp]: "extend_set h UNIV = UNIV"
 apply (unfold extend_set_def)
 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"
 by (auto intro: f_h_eq [symmetric] simp add: split_extended_all)
 

 
 lemma extend_set_subset_Compl_eq: "(extend_set h A \<subseteq> - extend_set h B) = (A \<subseteq> - B)"
   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')
   because h doesn't have to be injective in the 2nd argument*)
 lemma mem_extend_act_iff [iff]: "((h(s,y), h(s',y)) \<in> extend_act h act) = ((s, s') \<in> act)"