src/HOL/Library/Numeral_Type.thy
Fri, 08 Jan 2021 19:52:10 +0100 Manuel Eberl some algebra material for HOL: characteristic of a ring, algebraic integers
Thu, 17 Jan 2019 15:50:28 +0000 Angeliki KoutsoukouArgyraki more tagging
Wed, 16 Jan 2019 21:27:33 +0000 Angeliki KoutsoukouArgyraki updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
Wed, 16 Jan 2019 11:48:06 +0100 nipkow Reorg of material
Tue, 15 Jan 2019 21:31:20 +0100 nipkow moved and renamed class
Mon, 14 Jan 2019 18:35:03 +0000 haftmann tuned proofs
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 31 Oct 2018 15:53:32 +0100 wenzelm clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
Sat, 13 Jan 2018 09:18:54 +0000 haftmann restored naming of lemmas after corresponding constants
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Thu, 21 Dec 2017 18:11:24 +0100 nipkow tuned op's
Mon, 30 Oct 2017 13:18:41 +0000 haftmann tuned some proofs and added some lemmas
Fri, 20 Oct 2017 07:46:10 +0200 haftmann added lemmas and tuned proofs
Sat, 17 Dec 2016 15:22:14 +0100 haftmann reoriented congruence rules in non-explosive direction
Wed, 17 Feb 2016 21:51:57 +0100 haftmann dropped various legacy fact bindings
Fri, 13 Nov 2015 12:27:13 +0000 paulson Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
Thu, 05 Nov 2015 10:39:49 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 06 Jul 2015 22:57:34 +0200 wenzelm tuned proofs;
Wed, 17 Jun 2015 11:03:05 +0200 wenzelm isabelle update_cartouches;
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Sat, 15 Mar 2014 08:31:33 +0100 haftmann more complete set of lemmas wrt. image and composition
Sat, 25 Jan 2014 21:52:04 +0100 wenzelm prefer explicit 'for' context;
Sat, 25 May 2013 17:40:44 +0200 wenzelm tuned;
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Wed, 27 Feb 2013 10:33:30 +0100 Andreas Lochbihler add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Mon, 18 Feb 2013 08:52:23 +0100 Andreas Lochbihler simplify definition as sort constraints ensure finiteness (thanks to Jesus Aransay)
Fri, 15 Feb 2013 11:02:34 +0100 Andreas Lochbihler more type class instances for Numeral_Type (contributed by Jesus Aransay)
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Fri, 01 Jun 2012 11:53:58 +0200 huffman remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
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