| Sun, 04 Aug 2024 17:39:47 +0200 |
wenzelm |
tuned: more explicit dest_Const_name and dest_Const_type;
|
file |
diff |
annotate
|
| Sun, 04 Aug 2024 13:24:54 +0200 |
wenzelm |
tuned: more explicit dest_Type_name and dest_Type_args;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Fri, 30 Dec 2016 15:40:35 +0100 |
blanchet |
more uniform errors in '(prim)(co)rec(ursive)' variants
|
file |
diff |
annotate
|
| Wed, 28 Dec 2016 17:22:16 +0100 |
blanchet |
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
|
file |
diff |
annotate
|
| Mon, 12 Sep 2016 23:17:55 +0200 |
blanchet |
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
|
file |
diff |
annotate
|
| Thu, 01 Sep 2016 14:38:44 +0200 |
blanchet |
more robustness
|
file |
diff |
annotate
|
| Tue, 23 Aug 2016 15:19:32 +0200 |
traytel |
tuned signature
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 19:23:20 +0200 |
blanchet |
generalize code to avoid making assumptions about type variable names
|
file |
diff |
annotate
|
| Wed, 02 Mar 2016 10:02:12 +0100 |
traytel |
respect qualification when noting theorems in prim(co)rec
|
file |
diff |
annotate
|
| Tue, 16 Feb 2016 22:28:19 +0100 |
traytel |
make predicator a first-class bnf citizen
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 12:23:22 +0200 |
traytel |
{r,e,d,f}tac with proper context in BNF
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 19:05:00 +0200 |
blanchet |
have 'primrec' return definitions
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 18:23:01 +0200 |
blanchet |
renamed ML funs
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Sat, 07 Mar 2015 00:45:15 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Wed, 15 Oct 2014 17:15:11 +0200 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 21:41:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 18:45:48 +0200 |
wenzelm |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:43:26 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:54 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:15 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Wed, 17 Sep 2014 12:09:33 +0200 |
blanchet |
tweaked compatibility layer
|
file |
diff |
annotate
|
| Wed, 17 Sep 2014 08:23:53 +0200 |
blanchet |
support (finite values of) codatatypes in Quickcheck
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 12:11:41 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 10:49:07 +0200 |
blanchet |
generate 'code' attribute only if 'code' plugin is enabled
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:45:42 +0200 |
blanchet |
tuning terminology
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
speed up old Nominal by killing type variables
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 15:54:33 +0200 |
blanchet |
export right sorts
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:08 +0200 |
blanchet |
wildcards in plugins
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
improved 'datatype_compat' further for recursion through functions
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
no type-based lookup -- these fail in the general, ambiguous case
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
properly note theorems for split recursors
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
added 'plugins' option to control which hooks are enabled
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
tuned size function generation
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 22:49:05 +0200 |
blanchet |
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:06:19 +0200 |
blanchet |
more compatibility functions
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:06:18 +0200 |
blanchet |
codatatypes are not datatypes
|
file |
diff |
annotate
|
| Tue, 02 Sep 2014 12:11:04 +0200 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 19:58:25 +0200 |
blanchet |
avoid more 'bad background theory' issues
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 19:28:00 +0200 |
blanchet |
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 18:42:02 +0200 |
blanchet |
ported to use new-style datatypes
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 17:34:03 +0200 |
blanchet |
ported Refute to use new datatypes when possible
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:34:38 +0200 |
blanchet |
added primrec compatibility function
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
more work on compatibility interfaces
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
implemented compatibility definition of datatype
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
implemented compatibility interpretation
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
more compatibility between old- and new-style datatypes
|
file |
diff |
annotate
|