src/HOL/Tools/Datatype/datatype_case.ML
Wed, 28 Dec 2011 13:00:51 +0100 wenzelm print case syntax depending on "show_cases" configuration option;
Fri, 16 Dec 2011 11:02:55 +0100 wenzelm tuned;
Thu, 15 Dec 2011 19:53:28 +0100 wenzelm tuned;
Thu, 15 Dec 2011 18:08:40 +0100 wenzelm clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
Thu, 15 Dec 2011 14:11:57 +0100 wenzelm misc tuning and simplification;
Mon, 12 Dec 2011 23:05:21 +0100 wenzelm datatype dtyp with explicit sort information;
Fri, 02 Dec 2011 14:26:43 +0100 wenzelm eliminated some legacy operations;
Wed, 30 Nov 2011 21:14:01 +0100 wenzelm misc tuning;
Sun, 16 Oct 2011 18:48:30 +0200 wenzelm added Term.dummy_pattern conveniences;
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Wed, 08 Jun 2011 00:01:20 +0200 krauss eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
Wed, 08 Jun 2011 00:01:20 +0200 krauss more conventional variable naming
Wed, 08 Jun 2011 00:01:20 +0200 krauss dropped outdated/speculative historical comments;
Wed, 08 Jun 2011 00:01:20 +0200 krauss less redundant tags
Wed, 08 Jun 2011 00:01:20 +0200 krauss removed generation of instantiated pattern set, which is never actually used
Wed, 08 Jun 2011 00:01:20 +0200 krauss more precise type for obscure "prfx" field
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 15:25:25 +0200 wenzelm prefer local name spaces;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Tue, 22 Mar 2011 20:44:47 +0100 wenzelm more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
Tue, 22 Mar 2011 14:22:40 +0100 wenzelm datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
Tue, 22 Mar 2011 13:55:39 +0100 wenzelm tuned indendation and parentheses;
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Fri, 26 Feb 2010 23:08:45 +0100 wenzelm gen_dest_case: recovered @{const_name} from c8a6fae0ad0c, because of separate Syntax.mark_const in case_tr' -- avoid extra syntax markers in output;
Thu, 25 Feb 2010 22:17:33 +0100 wenzelm explicit @{type_syntax} markup;
Sun, 21 Feb 2010 22:35:02 +0100 wenzelm slightly more abstract syntax mark/unmark operations;
Sun, 21 Feb 2010 21:10:01 +0100 wenzelm adapted to authentic syntax;
Tue, 16 Feb 2010 11:56:13 +0100 wenzelm refrain from using @{const_name} in syntax translations;
Sun, 14 Feb 2010 00:26:48 +0100 wenzelm formal markup of constants;
Mon, 30 Nov 2009 12:28:12 +0100 haftmann dropped some unused bindings
Mon, 30 Nov 2009 11:42:49 +0100 haftmann modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
Wed, 21 Oct 2009 10:15:31 +0200 haftmann removed old-style \ and \\ infixes
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Thu, 08 Oct 2009 19:33:03 +0200 haftmann lookup for datatype constructors considers type annotations to resolve overloading
Wed, 23 Sep 2009 16:20:12 +0200 bulwahn adapted configuration for DatatypeCase.make_case
Fri, 17 Jul 2009 23:11:40 +0200 wenzelm tuned/modernized Envir.subst_XXX;
Tue, 23 Jun 2009 12:09:30 +0200 haftmann uniformly capitialized names for subdirectories
less more (0) tip