src/HOL/Library/Numeral_Type.thy
2009-02-19 huffman 2009-02-19 nicer induction/cases rules for numeral types
2009-02-19 huffman 2009-02-19 number_ring instances for numeral types
2009-01-26 haftmann 2009-01-26 tuned header
2008-12-09 huffman 2008-12-09 move lemmas from Numeral_Type.thy to other theories
2008-11-30 huffman 2008-11-30 fix typed print translation for card UNIV
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-04-02 chaieb 2008-04-02 No longer imports InfiniteSet, ATP_Linkup is sufficient.
2008-02-26 haftmann 2008-02-26 other UNIV lemmas
2007-11-23 haftmann 2007-11-23 deleted card definition as code lemma; authentic syntax for card
2007-11-10 wenzelm 2007-11-10 tuned document;
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-08-22 huffman 2007-08-22 typed print translation for CARD('a); declare zero_less_card_finite [simp]
2007-08-22 huffman 2007-08-22 rename type pls to num0
2007-08-20 kleing 2007-08-20 boolean algebras as locales and numbers as types by Brian Huffman