src/HOL/Library/Cardinality.thy
Tue, 15 Jan 2019 21:31:20 +0100 nipkow moved and renamed class
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Thu, 07 Jun 2018 19:36:12 +0200 nipkow utilize 'flip'
Tue, 24 Apr 2018 14:17:58 +0000 haftmann proper datatype for 8-bit characters
Fri, 20 Apr 2018 07:36:59 +0000 haftmann moved lemma to more appropriate place
Tue, 16 Jan 2018 09:30:00 +0100 wenzelm standardized towards new-style formal comments: isabelle update_comments;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Sat, 12 Mar 2016 22:04:52 +0100 haftmann model characters directly as range 0..255
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Thu, 05 Nov 2015 10:39:49 +0100 wenzelm isabelle update_cartouches -c -t;
Sun, 13 Sep 2015 20:20:16 +0200 wenzelm renamed method "goals" to "goal_cases" to emphasize its meaning;
Fri, 04 Sep 2015 19:22:13 +0200 wenzelm modernized name space management -- more uniform qualification;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Mon, 06 Jul 2015 22:57:34 +0200 wenzelm tuned proofs;
Fri, 26 Jun 2015 00:14:10 +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;
Fri, 20 Sep 2013 10:09:16 +0200 Andreas Lochbihler prefer Code.abort over code_abort
Sun, 25 Aug 2013 17:17:48 +0200 wenzelm tuned proofs -- fewer warnings;
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
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;
Tue, 19 Feb 2013 19:44:10 +0100 haftmann dropped spurious left-over from 0a2371e7ced3
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Fri, 15 Feb 2013 09:41:25 +0100 Andreas Lochbihler partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Thu, 14 Feb 2013 16:01:28 +0100 Andreas Lochbihler implement code generation for finite, card, op = and op <= for sets always via finite_UNIV and card_UNIV, as fragile rewrites based on sorts are hard to find and debug
Sat, 20 Oct 2012 09:12:16 +0200 haftmann moved quite generic material from theory Enum to more appropriate places
Wed, 03 Oct 2012 16:59:20 +0200 wenzelm recovered print translation after 'a => bool to 'a set change;
Tue, 03 Jul 2012 09:26:52 +0200 Andreas Lochbihler new type class for computing finiteness of types with instantiations
Thu, 28 Jun 2012 09:18:58 +0200 Andreas Lochbihler instantiate card_UNIV with nibble and code_numeral
Thu, 28 Jun 2012 09:16:00 +0200 Andreas Lochbihler change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Mon, 04 Jun 2012 09:50:57 +0200 Andreas Lochbihler more sort constraints for FinFun code generation
Sat, 02 Jun 2012 08:32:42 +0200 huffman merged
Fri, 01 Jun 2012 11:53:58 +0200 huffman remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
Fri, 01 Jun 2012 20:40:34 +0200 Andreas Lochbihler improved code setup for card, finite, subset
Fri, 01 Jun 2012 15:33:31 +0200 Andreas Lochbihler more instantiations for card_UNIV,
Fri, 01 Jun 2012 14:34:46 +0200 Andreas Lochbihler simplify card_UNIV type class,
Fri, 01 Jun 2012 13:52:51 +0200 Andreas Lochbihler drop redundant sort constraint
Thu, 31 May 2012 17:10:43 +0200 Andreas Lochbihler tuned proofs
Thu, 31 May 2012 17:04:11 +0200 Andreas Lochbihler tuned instantiations
Thu, 31 May 2012 16:58:38 +0200 Andreas Lochbihler unify Card_Univ and Cardinality
Fri, 30 Mar 2012 14:00:18 +0200 huffman rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Wed, 10 Aug 2011 18:02:16 -0700 huffman avoid warnings about duplicate rules
Wed, 06 Apr 2011 13:33:46 +0200 wenzelm typed_print_translation: discontinued show_sorts argument;
Wed, 06 Apr 2011 12:58:13 +0200 wenzelm moved unparse material to syntax_phases.ML;
Wed, 30 Jun 2010 16:28:13 +0200 haftmann split off Cardinality from Numeral_Type
less more (0) tip