Thu, 06 Mar 2014 12:10:19 +0100 |
wenzelm |
tuned signature -- more uniform check_type_name/read_type_name;
|
file |
diff |
annotate
|
Wed, 26 Feb 2014 10:53:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 17:36:00 +0100 |
blanchet |
iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
|
file |
diff |
annotate
|
Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
generate 'disc_iff' property in 'primcorec'
|
file |
diff |
annotate
|
Tue, 19 Nov 2013 14:33:20 +0100 |
blanchet |
case_if -> case_eq_if + docs
|
file |
diff |
annotate
|
Wed, 13 Nov 2013 12:32:26 +0100 |
blanchet |
shortened generated property name
|
file |
diff |
annotate
|
Tue, 12 Nov 2013 13:47:24 +0100 |
blanchet |
register old-style datatypes as 'Ctr_Sugar'
|
file |
diff |
annotate
|
Thu, 15 Dec 2011 18:08:40 +0100 |
wenzelm |
clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
|
file |
diff |
annotate
|
Thu, 15 Dec 2011 17:37:14 +0100 |
wenzelm |
separate rep_datatype.ML;
|
file |
diff |
annotate
|
Thu, 15 Dec 2011 14:11:57 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
Wed, 14 Dec 2011 22:10:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 14 Dec 2011 21:54:32 +0100 |
wenzelm |
avoid fragile Sign.intern_const -- pass internal names directly;
|
file |
diff |
annotate
|
Tue, 13 Dec 2011 23:23:51 +0100 |
wenzelm |
'datatype' specifications allow explicit sort constraints;
|
file |
diff |
annotate
|
Mon, 12 Dec 2011 23:05:21 +0100 |
wenzelm |
datatype dtyp with explicit sort information;
|
file |
diff |
annotate
|
Mon, 12 Dec 2011 20:55:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 02 Dec 2011 14:26:43 +0100 |
wenzelm |
eliminated some legacy operations;
|
file |
diff |
annotate
|
Wed, 30 Nov 2011 23:30:08 +0100 |
wenzelm |
discontinued obsolete datatype "alt_names";
|
file |
diff |
annotate
|
Wed, 30 Nov 2011 21:14:01 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
Wed, 23 Nov 2011 22:59:39 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
Wed, 09 Nov 2011 21:36:18 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 22:44:44 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 17:04:04 +0200 |
krauss |
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 22:20:49 +0200 |
wenzelm |
document antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
removed generation of instantiated pattern set, which is never actually used
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 15:25:25 +0200 |
wenzelm |
prefer local name spaces;
|
file |
diff |
annotate
|
Fri, 08 Apr 2011 21:11:29 +0200 |
wenzelm |
discontinued Syntax.max_pri, which is not really a symbolic parameter;
|
file |
diff |
annotate
|
Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
Fri, 08 Apr 2011 15:48:14 +0200 |
wenzelm |
discontinued special status of structure Printer;
|
file |
diff |
annotate
|
Mon, 10 Jan 2011 15:19:48 +0100 |
wenzelm |
standardized split_last/last_elem towards List.last;
|
file |
diff |
annotate
|
Thu, 30 Dec 2010 23:42:06 +0100 |
wenzelm |
do not open auxiliary ML structures;
|
file |
diff |
annotate
|
Sat, 04 Dec 2010 14:59:25 +0100 |
wenzelm |
tuned @{datatype} using Syntax.pretty_priority (NB: postfix type application yields Syntax.max_pri, so arguments in prefix application require higher priority);
|
file |
diff |
annotate
|
Fri, 03 Dec 2010 10:03:13 +0100 |
huffman |
theorem names generated by the (rep_)datatype command now have mandatory qualifiers
|
file |
diff |
annotate
|
Wed, 01 Dec 2010 15:03:44 +0100 |
wenzelm |
more direct use of binder_types/body_type;
|
file |
diff |
annotate
|
Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
Fri, 27 Aug 2010 12:40:20 +0200 |
wenzelm |
proper context for various Thy_Output options, via official configuration options in ML and Isar;
|
file |
diff |
annotate
|
Thu, 26 Aug 2010 13:09:12 +0200 |
wenzelm |
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
|
file |
diff |
annotate
|
Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
Fri, 30 Apr 2010 23:43:09 +0200 |
wenzelm |
slightly more standard induct_simp_add/del attributes;
|
file |
diff |
annotate
|
Sun, 25 Apr 2010 15:52:03 +0200 |
wenzelm |
modernized naming conventions of main Isar proof elements;
|
file |
diff |
annotate
|
Thu, 25 Feb 2010 22:06:43 +0100 |
wenzelm |
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
|
file |
diff |
annotate
|
Sun, 21 Feb 2010 22:35:02 +0100 |
wenzelm |
slightly more abstract syntax mark/unmark operations;
|
file |
diff |
annotate
|
Sun, 21 Feb 2010 21:10:01 +0100 |
wenzelm |
adapted to authentic syntax;
|
file |
diff |
annotate
|
Sun, 14 Feb 2010 00:26:48 +0100 |
wenzelm |
formal markup of constants;
|
file |
diff |
annotate
|
Sun, 10 Jan 2010 18:11:00 +0100 |
berghofe |
Injectivity / distinctness theorems are now used to simplify induction rules.
|
file |
diff |
annotate
|
Wed, 02 Dec 2009 11:29:49 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
| base
|
Mon, 30 Nov 2009 12:28:12 +0100 |
haftmann |
dropped some unused bindings
|
file |
diff |
annotate
| base
|
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
|
file |
diff |
annotate
| base
|
Fri, 27 Nov 2009 08:42:34 +0100 |
haftmann |
renamed former datatype.ML to datatype_data.ML
|
file |
diff |
annotate
| base
|
Fri, 27 Nov 2009 08:41:10 +0100 |
haftmann |
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
| base
|