src/HOL/Library/Numeral_Type.thy
Sun, 11 Mar 2012 13:54:08 +0100 wenzelm eliminated old-fashioned 'constrains' element;
Mon, 16 Jan 2012 21:50:15 +0100 wenzelm position constraints for numerals enable PIDE markup;
Wed, 30 Jun 2010 16:28:13 +0200 haftmann split off Cardinality from Numeral_Type
Mon, 26 Apr 2010 11:34:19 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps
Wed, 03 Mar 2010 00:33:02 +0100 wenzelm cleanup type translations;
Thu, 25 Feb 2010 22:15:27 +0100 wenzelm explicit @{type_syntax} markup;
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
Fri, 30 Oct 2009 14:00:43 +0100 haftmann combined former theories Divides and IntDiv to one theory Divides
Wed, 21 Oct 2009 00:36:12 +0200 wenzelm standardized basic operations on type option;
Sat, 09 May 2009 07:25:22 +0200 nipkow lemmas by Andreas Lochbihler
Wed, 29 Apr 2009 14:20:26 +0200 haftmann farewell to class recpower
Wed, 22 Apr 2009 19:09:21 +0200 haftmann power operation defined generic
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default;
Mon, 23 Mar 2009 08:14:24 +0100 haftmann Main is (Complex_Main) base entry point in library theories
Fri, 13 Mar 2009 07:35:18 -0700 huffman fix typed print translation for CARD('a)
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Fri, 20 Feb 2009 11:58:00 -0800 huffman class instances for num1
Thu, 19 Feb 2009 23:18:28 -0800 huffman cleaned up
Thu, 19 Feb 2009 17:13:35 -0800 huffman fix case_names
Thu, 19 Feb 2009 17:11:12 -0800 huffman nicer induction/cases rules for numeral types
Thu, 19 Feb 2009 16:51:46 -0800 huffman number_ring instances for numeral types
Mon, 26 Jan 2009 22:14:17 +0100 haftmann tuned header
Tue, 09 Dec 2008 15:31:38 -0800 huffman move lemmas from Numeral_Type.thy to other theories
Sun, 30 Nov 2008 18:10:00 +0100 huffman fix typed print translation for card UNIV
Mon, 07 Jul 2008 08:47:17 +0200 haftmann absolute imports of HOL/*.thy theories
Thu, 26 Jun 2008 10:07:01 +0200 haftmann established Plain theory and image
Wed, 02 Apr 2008 12:32:53 +0200 chaieb No longer imports InfiniteSet, ATP_Linkup is sufficient.
Tue, 26 Feb 2008 20:38:18 +0100 haftmann other UNIV lemmas
Fri, 23 Nov 2007 21:09:32 +0100 haftmann deleted card definition as code lemma; authentic syntax for card
Sat, 10 Nov 2007 18:36:06 +0100 wenzelm tuned document;
Tue, 18 Sep 2007 16:08:00 +0200 wenzelm simplified type int (eliminated IntInf.int, integer);
Wed, 22 Aug 2007 20:59:19 +0200 huffman typed print translation for CARD('a);
Wed, 22 Aug 2007 18:53:54 +0200 huffman rename type pls to num0
Mon, 20 Aug 2007 00:22:18 +0200 kleing boolean algebras as locales and numbers as types by Brian Huffman
less more (0) tip