src/HOL/Order_Relation.thy

 
 
 subsubsection \<open>The upper and lower bounds operators\<close>
 
 text\<open>Here we define upper (``above") and lower (``below") bounds operators.
-We think of @{text "r"} as a {\em non-strict} relation.  The suffix ``S"
+We think of \<open>r\<close> as a {\em non-strict} relation.  The suffix ``S"
 at the names of some operators indicates that the bounds are strict -- e.g.,
-@{text "underS a"} is the set of all strict lower bounds of @{text "a"} (w.r.t. @{text "r"}).
+\<open>underS a\<close> is the set of all strict lower bounds of \<open>a\<close> (w.r.t. \<open>r\<close>).
 Capitalization of the first letter in the name reminds that the operator acts on sets, rather
 than on individual elements.\<close>
 
 definition under::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
 where "under r a \<equiv> {b. (b,a) \<in> r}"

 where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
 
 definition ofilter :: "'a rel \<Rightarrow> 'a set \<Rightarrow> bool"
 where "ofilter r A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under r a \<le> A)"
 
-text\<open>Note:  In the definitions of @{text "Above[S]"} and @{text "Under[S]"},
-  we bounded comprehension by @{text "Field r"} in order to properly cover
-  the case of @{text "A"} being empty.\<close>
+text\<open>Note:  In the definitions of \<open>Above[S]\<close> and \<open>Under[S]\<close>,
+  we bounded comprehension by \<open>Field r\<close> in order to properly cover
+  the case of \<open>A\<close> being empty.\<close>
 
 lemma underS_subset_under: "underS r a \<le> under r a"
 by(auto simp add: underS_def under_def)
 
 lemma underS_notIn: "a \<notin> underS r a"

    qed
   }
   ultimately show ?thesis using R_def by blast
 qed
 
-text \<open>The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded,
+text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded,
 allowing one to assume the set included in the field.\<close>
 
 lemma wf_eq_minimal2:
 "wf r = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))"
 proof-