src/HOL/Library/Numeral_Type.thy
changeset 25459 d1dce7d0731c
parent 25378 dca691610489
child 26153 b037fd9016fa
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Fri Nov 23 21:09:30 2007 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Fri Nov 23 21:09:32 2007 +0100
     1.3 @@ -52,7 +52,7 @@
     1.4  
     1.5  syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
     1.6  
     1.7 -translations "CARD(t)" => "card (UNIV::t set)"
     1.8 +translations "CARD(t)" => "CONST card (UNIV \<Colon> t set)"
     1.9  
    1.10  typed_print_translation {*
    1.11  let
    1.12 @@ -239,8 +239,6 @@
    1.13  
    1.14  subsection {* Examples *}
    1.15  
    1.16 -term "TYPE(10)"
    1.17 -
    1.18  lemma "CARD(0) = 0" by simp
    1.19  lemma "CARD(17) = 17" by simp
    1.20