[isabelle-dev] Numeral_Type.thy

Brian Huffman brianh at cs.pdx.edu
Thu Mar 12 20:00:30 CET 2009


The typed print translation in Numeral_Type.thy, which prints "card  
(UNIV :: 'a set)" as "CARD('a)", is broken.

I think it has something to do with the new properly-qualified name  
for "UNIV" that was introduced recently.

Anyway, I'm not exactly sure what is going wrong or how to fix it.  
Does anyone have an idea?

- Brian




More information about the isabelle-dev mailing list