| Sat, 16 Aug 2014 22:14:57 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:14:58 +0200 |
blanchet |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
localize new size function generation code
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
put theorems in right slot
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
move size hooks together, with new one preceding old one and sharing same theory data
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
|
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
|
| Fri, 21 Mar 2014 10:45:03 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 21 Jan 2014 13:05:22 +0100 |
blanchet |
removed dependency on 'Datatype' structure
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 14:19:18 +0100 |
wenzelm |
tuned signature and module arrangement;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2012 22:11:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 24 Jan 2012 16:00:51 +0100 |
berghofe |
Use lookup_size rather than Datatype.get_info in is_poly to avoid
|
file |
diff |
annotate
|
| Fri, 16 Dec 2011 21:23:21 +0100 |
wenzelm |
eliminated old-fashioned Global_Theory.add_thms(s);
|
file |
diff |
annotate
|
| Fri, 16 Dec 2011 10:38:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 12 Dec 2011 23:05:21 +0100 |
wenzelm |
datatype dtyp with explicit sort information;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 13:51:36 +0100 |
wenzelm |
do not open ML structures;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 13:38:24 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 23:30:08 +0100 |
wenzelm |
discontinued obsolete datatype "alt_names";
|
file |
diff |
annotate
|
| Tue, 31 May 2011 11:21:47 +0200 |
krauss |
more precise authorship, reflecting my own ignorance and hg annotate
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 30 Dec 2010 23:42:06 +0100 |
wenzelm |
do not open auxiliary ML structures;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 21:31:46 +0100 |
wenzelm |
explicit use of unprefix;
|
file |
diff |
annotate
|
| Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
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
|
| Wed, 11 Aug 2010 14:31:43 +0200 |
haftmann |
moved instantiation target formally to class_target.ML
|
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, 12 Mar 2010 12:14:30 +0100 |
bulwahn |
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
|
file |
diff |
annotate
|