# HG changeset patch
# User haftmann
# Date 1195848572 -3600
# Node ID d1dce7d0731c4caa1b6ecce84d8ace0b623ee5bd
# Parent  ba8f5e4fa33642dd2f94a4f6e15d5374e1dac060
deleted card definition as code lemma; authentic syntax for card

diff -r ba8f5e4fa336 -r d1dce7d0731c NEWS
--- 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
diff -r ba8f5e4fa336 -r d1dce7d0731c src/HOL/Finite_Set.thy
--- 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)
diff -r ba8f5e4fa336 -r d1dce7d0731c src/HOL/Library/Numeral_Type.thy
--- 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