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