changeset 61076 | bdc1e2f0a86a |
parent 60679 | ade12ef2773c |
child 61115 | 3a4400985780 |
--- a/src/HOL/Library/Cardinality.thy Tue Sep 01 17:25:36 2015 +0200 +++ b/src/HOL/Library/Cardinality.thy Tue Sep 01 22:32:58 2015 +0200 @@ -41,7 +41,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 :: 't set)" print_translation \<open> let