--- a/NEWS Fri Nov 23 21:09:30 2007 +0100
+++ b/NEWS Fri Nov 23 21:09:32 2007 +0100
@@ -548,6 +548,8 @@
*** HOL ***
+* Constant "card" now with authentic syntax.
+
* Method "metis" proves goals by applying the Metis general-purpose
resolution prover (see also http://gilith.com/software/metis/).
Examples are in the directory MetisExamples. WARNING: the
--- a/src/HOL/Finite_Set.thy Fri Nov 23 21:09:30 2007 +0100
+++ b/src/HOL/Finite_Set.thy Fri Nov 23 21:09:32 2007 +0100
@@ -1500,9 +1500,10 @@
But now that we have @{text setsum} things are easy:
*}
-constdefs
- card :: "'a set => nat"
- "card A == setsum (%x. 1::nat) A"
+definition
+ card :: "'a set \<Rightarrow> nat"
+where
+ [code func del]: "card A = setsum (\<lambda>x. 1) A"
lemma card_empty [simp]: "card {} = 0"
by (simp add: card_def)
--- a/src/HOL/Library/Numeral_Type.thy Fri Nov 23 21:09:30 2007 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Fri Nov 23 21:09:32 2007 +0100
@@ -52,7 +52,7 @@
syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
-translations "CARD(t)" => "card (UNIV::t set)"
+translations "CARD(t)" => "CONST card (UNIV \<Colon> t set)"
typed_print_translation {*
let
@@ -239,8 +239,6 @@
subsection {* Examples *}
-term "TYPE(10)"
-
lemma "CARD(0) = 0" by simp
lemma "CARD(17) = 17" by simp