--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Nov 25 12:27:03 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Nov 25 13:48:00 2013 +0100
@@ -183,22 +183,4 @@
lemma cpow_cexp_ctwo: "cpow r =o ctwo ^c r"
unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)
-
-subsection {* Lists *}
-
-text {*
- The following collection of lemmas should be seen as an user interface to the HOL theory
- of cardinals. It is not expected to be complete in any sense, since its
- development was driven by demand arising from the development of the (co)datatype package.
-*}
-
-lemma clists_Cinfinite: "Cinfinite r \<Longrightarrow> clists r =o r"
-unfolding cinfinite_def clists_def by (blast intro: Card_order_lists_infinite)
-
-lemma Card_order_clists: "Card_order (clists r)"
-unfolding clists_def by (rule card_of_Card_order)
-
-lemma Cnotzero_clists: "Cnotzero (clists r)"
-by (simp add: clists_def card_of_ordIso_czero_iff_empty lists_not_empty)
-
end