| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
tuned structure inclusion
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 17:19:58 +0200 |
blanchet |
reordered some (co)datatype property names for more consistency
|
file |
diff |
annotate
|
| Mon, 05 May 2014 09:30:20 +0200 |
blanchet |
simplify selectors in code views
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 10:51:22 +0200 |
blanchet |
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 12:43:29 +0100 |
wenzelm |
more rigid type_name demands, based on educated guesses about the tools involved here;
|
file |
diff |
annotate
|
| 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
|