| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Mon, 30 Apr 2012 22:18:39 +1000 |
Gerwin Klein |
provide [[record_codegen]] option for skipping codegen setup for records
|
file |
diff |
annotate
|
| Sun, 15 Jan 2012 20:30:17 +0100 |
wenzelm |
tuned example;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 13:00:19 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 17:09:35 +0200 |
haftmann |
delete structure Basic_Record; avoid `record` in names in structure Record
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 16:13:14 +0200 |
haftmann |
avoid export_code ... file -
|
file |
diff |
annotate
|
| Wed, 27 Jan 2010 14:02:53 +0100 |
haftmann |
a more complex record expression -- cf. src/HOL/Tools/quickcheck_generators.ML
|
file |
diff |
annotate
|
| Wed, 11 Nov 2009 15:10:29 +0100 |
haftmann |
explicit invocation of code generation
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 16:11:46 +0100 |
haftmann |
tuned header
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| Sun, 24 May 2009 15:02:22 +0200 |
haftmann |
dropped Id
|
file |
diff |
annotate
|
| Sat, 17 May 2008 21:46:22 +0200 |
wenzelm |
avoid undeclared variables within proofs;
|
file |
diff |
annotate
|
| Wed, 19 Dec 2007 16:32:16 +0100 |
schirmer |
more examples
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:35 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Sat, 27 May 2006 17:42:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Tue, 29 Jun 2004 11:18:34 +0200 |
kleing |
license change to BSD
|
file |
diff |
annotate
|
| Mon, 03 May 2004 23:22:17 +0200 |
schirmer |
reimplementation of HOL records; only one type is created for
|
file |
diff |
annotate
|
| Fri, 21 Dec 2001 23:18:46 +0100 |
wenzelm |
qualified point.more;
|
file |
diff |
annotate
|
| Thu, 22 Nov 2001 17:13:24 +0100 |
wenzelm |
thm "point.defs";
|
file |
diff |
annotate
|
| Thu, 25 Oct 2001 22:43:05 +0200 |
wenzelm |
updated records;
|
file |
diff |
annotate
|
| Thu, 25 Oct 2001 02:11:49 +0200 |
wenzelm |
(simp add: point.make_def);
|
file |
diff |
annotate
|
| Sat, 06 Oct 2001 00:02:46 +0200 |
wenzelm |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Mon, 30 Oct 2000 18:24:42 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2000 15:58:13 +0200 |
wenzelm |
renamed HOL/ex/Points to HOL/ex/Records;
|
file |
diff |
annotate
|