src/HOL/Library/Numeral_Type.thy
2016-12-17 haftmann 2016-12-17 reoriented congruence rules in non-explosive direction
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-01-25 wenzelm 2014-01-25 prefer explicit 'for' context;
2013-05-25 wenzelm 2013-05-25 tuned;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-02-27 Andreas Lochbihler 2013-02-27 add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
2013-02-18 Andreas Lochbihler 2013-02-18 simplify definition as sort constraints ensure finiteness (thanks to Jesus Aransay)
2013-02-15 Andreas Lochbihler 2013-02-15 more type class instances for Numeral_Type (contributed by Jesus Aransay)
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-06-01 huffman 2012-06-01 remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-11 wenzelm 2012-03-11 eliminated old-fashioned 'constrains' element;
2012-01-16 wenzelm 2012-01-16 position constraints for numerals enable PIDE markup;
2010-06-30 haftmann 2010-06-30 split off Cardinality from Numeral_Type
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-03-03 wenzelm 2010-03-03 cleanup type translations;
2010-02-25 wenzelm 2010-02-25 explicit @{type_syntax} markup; misc tuning and simplification;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2009-10-30 haftmann 2009-10-30 combined former theories Divides and IntDiv to one theory Divides
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-05-09 nipkow 2009-05-09 lemmas by Andreas Lochbihler
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-04-22 haftmann 2009-04-22 power operation defined generic
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-03-13 huffman 2009-03-13 fix typed print translation for CARD('a)
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-20 huffman 2009-02-20 class instances for num1
2009-02-19 huffman 2009-02-19 cleaned up
2009-02-19 huffman 2009-02-19 fix case_names
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