# 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 \ nat" +where + [code func del]: "card A = setsum (\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 \ 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