src/HOL/Finite_Set.thy

   unfolding Finite_Set.fold_def
   by (subst fold_graph_closed_eq[where B=B and g=g]) (auto simp: that)
 
 text \<open>
   A tempting alternative for the definiens is
-  @{term "if finite A then THE y. fold_graph f z A y else e"}.
+  \<^term>\<open>if finite A then THE y. fold_graph f z A y else e\<close>.
   It allows the removal of finiteness assumptions from the theorems
   \<open>fold_comm\<close>, \<open>fold_reindex\<close> and \<open>fold_distrib\<close>.
   The proofs become ugly. It is not worth the effort. (???)
 \<close>
 
 lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x"
   by (induct rule: finite_induct) auto
 
 
-subsubsection \<open>From @{const fold_graph} to @{term fold}\<close>
+subsubsection \<open>From \<^const>\<open>fold_graph\<close> to \<^term>\<open>fold\<close>\<close>
 
 context comp_fun_commute
 begin
 
 lemma fold_graph_finite:

   by (auto simp: fold_def)
 
 lemma (in -) fold_empty [simp]: "fold f z {} = z"
   by (auto simp: fold_def)
 
-text \<open>The various recursion equations for @{const fold}:\<close>
+text \<open>The various recursion equations for \<^const>\<open>fold\<close>:\<close>
 
 lemma fold_insert [simp]:
   assumes "finite A" and "x \<notin> A"
   shows "fold f z (insert x A) = f x (fold f z A)"
 proof (rule fold_equality)

   shows "Finite_Set.fold f z (A \<union> B) = Finite_Set.fold f (Finite_Set.fold f z A) B"
   using assms(2,1,3) by induct simp_all
 
 end
 
-text \<open>Other properties of @{const fold}:\<close>
+text \<open>Other properties of \<^const>\<open>fold\<close>:\<close>
 
 lemma fold_image:
   assumes "inj_on g A"
   shows "fold f z (g ` A) = fold (f \<circ> g) z A"
 proof (cases "finite A")

     qed
   qed
 qed
 
 
-subsubsection \<open>Expressing set operations via @{const fold}\<close>
+subsubsection \<open>Expressing set operations via \<^const>\<open>fold\<close>\<close>
 
 lemma comp_fun_commute_const: "comp_fun_commute (\<lambda>_. f)"
   by standard rule
 
 lemma comp_fun_idem_insert: "comp_fun_idem insert"

 
 subsection \<open>Finite cardinality\<close>
 
 text \<open>
   The traditional definition
-  @{prop "card A \<equiv> LEAST n. \<exists>f. A = {f i |i. i < n}"}
+  \<^prop>\<open>card A \<equiv> LEAST n. \<exists>f. A = {f i |i. i < n}\<close>
   is ugly to work with.
-  But now that we have @{const fold} things are easy:
+  But now that we have \<^const>\<open>fold\<close> things are easy:
 \<close>
 
 global_interpretation card: folding "\<lambda>_. Suc" 0
   defines card = "folding.F (\<lambda>_. Suc) 0"
   by standard rule