# HG changeset patch
# User wenzelm
# Date 1380372106 -7200
# Node ID 7ed81754b0696cd94fc76dee3b4c38cb137699c8
# Parent  814dbc4e84a30ad4e3a4c6b1452adc45a722f8f1
proper document markup;

diff -r 814dbc4e84a3 -r 7ed81754b069 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Sat Sep 28 14:36:04 2013 +0200
+++ b/src/HOL/Library/FSet.thy	Sat Sep 28 14:41:46 2013 +0200
@@ -432,11 +432,11 @@
 
 subsection {* Additional lemmas*}
 
-subsubsection {* fsingleton *}
+subsubsection {* @{text fsingleton} *}
 
 lemmas fsingletonE = fsingletonD [elim_format]
 
-subsubsection {* femepty *}
+subsubsection {* @{text femepty} *}
 
 lemma fempty_ffilter[simp]: "ffilter (\<lambda>_. False) A = {||}"
 by transfer auto
@@ -445,7 +445,7 @@
 lemma femptyE [elim!]: "a |\<in>| {||} \<Longrightarrow> P"
   by simp
 
-subsubsection {* fset *}
+subsubsection {* @{text fset} *}
 
 lemmas fset_simps[simp] = bot_fset.rep_eq finsert.rep_eq
 
@@ -467,7 +467,7 @@
 
 lemmas minus_fset[simp] = minus_fset.rep_eq
 
-subsubsection {* filter_fset *}
+subsubsection {* @{text filter_fset} *}
 
 lemma subset_ffilter: 
   "ffilter P A |\<subseteq>| ffilter Q A = (\<forall> x. x |\<in>| A \<longrightarrow> P x \<longrightarrow> Q x)"
@@ -482,7 +482,7 @@
     ffilter P A |\<subset>| ffilter Q A"
   unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter)
 
-subsubsection {* finsert *}
+subsubsection {* @{text finsert} *}
 
 (* FIXME, transferred doesn't work here *)
 lemma set_finsert:
@@ -493,7 +493,7 @@
 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 {* fimage *}
+subsubsection {* @{text fimage} *}
 
 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)
@@ -528,7 +528,7 @@
 
 end
 
-subsubsection {* fcard *}
+subsubsection {* @{text fcard} *}
 
 (* FIXME: improve transferred to handle bounded meta quantification *)
 
@@ -610,7 +610,7 @@
 lemma fcard_pfsubset: "A |\<subseteq>| B \<Longrightarrow> fcard A < fcard B \<Longrightarrow> A < B"
 by transfer (rule card_psubset)
 
-subsubsection {* ffold *}
+subsubsection {* @{text ffold} *}
 
 (* FIXME: improve transferred to handle bounded meta quantification *)