src/HOL/Library/FSet.thy

 lemmas fequalityI = equalityI[Transfer.transferred]
 
 
 subsection \<open>Additional lemmas\<close>
 
-subsubsection \<open>@{text fsingleton}\<close>
+subsubsection \<open>\<open>fsingleton\<close>\<close>
 
 lemmas fsingletonE = fsingletonD [elim_format]
 
 
-subsubsection \<open>@{text femepty}\<close>
+subsubsection \<open>\<open>femepty\<close>\<close>
 
 lemma fempty_ffilter[simp]: "ffilter (\<lambda>_. False) A = {||}"
 by transfer auto
 
 (* FIXME, transferred doesn't work here *)
 lemma femptyE [elim!]: "a |\<in>| {||} \<Longrightarrow> P"
   by simp
 
 
-subsubsection \<open>@{text fset}\<close>
+subsubsection \<open>\<open>fset\<close>\<close>
 
 lemmas fset_simps[simp] = bot_fset.rep_eq finsert.rep_eq
 
 lemma finite_fset [simp]: 
   shows "finite (fset S)"

 lemmas union_fset[simp] = sup_fset.rep_eq
 
 lemmas minus_fset[simp] = minus_fset.rep_eq
 
 
-subsubsection \<open>@{text filter_fset}\<close>
+subsubsection \<open>\<open>filter_fset\<close>\<close>
 
 lemma subset_ffilter: 
   "ffilter P A |\<subseteq>| ffilter Q A = (\<forall> x. x |\<in>| A \<longrightarrow> P x \<longrightarrow> Q x)"
   by transfer auto
 

   "(\<And>x. x |\<in>| A \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| A & \<not> P x & Q x) \<Longrightarrow> 
     ffilter P A |\<subset>| ffilter Q A"
   unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter)
 
 
-subsubsection \<open>@{text finsert}\<close>
+subsubsection \<open>\<open>finsert\<close>\<close>
 
 (* FIXME, transferred doesn't work here *)
 lemma set_finsert:
   assumes "x |\<in>| A"
   obtains B where "A = finsert x B" and "x |\<notin>| B"

 
 lemma mk_disjoint_finsert: "a |\<in>| A \<Longrightarrow> \<exists>B. A = finsert a B \<and> a |\<notin>| B"
   by (rule_tac x = "A |-| {|a|}" in exI, blast)
 
 
-subsubsection \<open>@{text fimage}\<close>
+subsubsection \<open>\<open>fimage\<close>\<close>
 
 lemma subset_fimage_iff: "(B |\<subseteq>| f|`|A) = (\<exists> AA. AA |\<subseteq>| A \<and> B = f|`|AA)"
 by transfer (metis mem_Collect_eq rev_finite_subset subset_image_iff)
 
 

 by (transfer, simp)+
 
 end
 
 
-subsubsection \<open>@{text fcard}\<close>
+subsubsection \<open>\<open>fcard\<close>\<close>
 
 (* FIXME: improve transferred to handle bounded meta quantification *)
 
 lemma fcard_fempty:
   "fcard {||} = 0"

 
 lemma fcard_pfsubset: "A |\<subseteq>| B \<Longrightarrow> fcard A < fcard B \<Longrightarrow> A < B"
 by transfer (rule card_psubset)
 
 
-subsubsection \<open>@{text ffold}\<close>
+subsubsection \<open>\<open>ffold\<close>\<close>
 
 (* FIXME: improve transferred to handle bounded meta quantification *)
 
 context comp_fun_commute
 begin