src/HOL/Library/Numeral_Type.thy
changeset 35431 8758fe1fc9f8
parent 35362 828a42fb7445
child 36350 bc7982c54e37
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Wed Mar 03 00:32:14 2010 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Mar 03 00:33:02 2010 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  
     1.5  syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
     1.6  
     1.7 -translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"
     1.8 +translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
     1.9  
    1.10  typed_print_translation {*
    1.11  let