| Sun, 26 Jul 2015 17:24:54 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2015 16:13:03 +0200 |
traytel |
forgotten selector
|
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
|
| Tue, 28 Apr 2015 22:57:07 +0200 |
blanchet |
allow sorts on dead variables in BNFs
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2015 22:34:59 +0200 |
wenzelm |
support for strictly private name space entries;
|
file |
diff |
annotate
|
| Fri, 27 Mar 2015 09:56:34 +0100 |
blanchet |
sort BNFs in output
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 23:05:56 +0100 |
traytel |
BNF relators preserve reflexivity
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 09:49:17 +0100 |
blanchet |
split into subgoals
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 10:09:42 +0100 |
blanchet |
added plugins syntax to prim(co)rec
|
file |
diff |
annotate
|
| Thu, 11 Dec 2014 14:14:39 +0100 |
traytel |
note more facts (always)
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 19:34:10 +0200 |
wenzelm |
clarified load order;
|
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
|
| Wed, 24 Sep 2014 16:35:42 +0200 |
blanchet |
improved 'bnf' parser
|
file |
diff |
annotate
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
register 'prod' and 'sum' as datatypes, to allow N2M through them
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 16:14:14 +0200 |
blanchet |
set 'mono' attribute on 'rel_mono'
|
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 |
introduced mechanism to filter interpretations
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
fixed infinite loops in 'register' functions + more uniform API
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:00 +0200 |
blanchet |
centralized and cleaned up naming handling
|
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 22:47:35 +0200 |
blanchet |
tuned BNF database handling
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
added theory-based getters for convenience
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 13:53:34 +0200 |
desharna |
generate 'set_transfer' for BNFs
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 13:23:39 +0200 |
desharna |
generate 'rel_transfer' for BNFs
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 13:23:00 +0200 |
desharna |
note 'map_transfer' more often
|
file |
diff |
annotate
|
| Fri, 29 Aug 2014 14:21:24 +0200 |
desharna |
generate 'case_transfer' for (co)datatypes
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 15:03:22 +0200 |
desharna |
generate 'map_cong_simp' for BNFs
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 14:09:09 +0200 |
desharna |
generate 'inj_map_strong' for BNFs
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 13:49:47 +0200 |
desharna |
note 'inj_map' more often
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 13:46:26 +0200 |
desharna |
generate property 'rel_mono_strong' for BNFs
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 13:46:22 +0200 |
desharna |
renamed 'rel_mono_strong' to 'rel_mono_strong0'
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 13:20:54 +0200 |
desharna |
generate 'rel_map' theorem for BNFs
|
file |
diff |
annotate
|
| Fri, 25 Jul 2014 11:26:10 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use the noted theorems in 'BNF_Comp'
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use the noted theorem whenever possible, also in 'BNF_Def'
|
file |
diff |
annotate
|
| Thu, 17 Jul 2014 10:28:32 +0200 |
desharna |
add mk_Trueprop_mem utility function
|
file |
diff |
annotate
|
| Wed, 09 Jul 2014 11:35:52 +0200 |
blanchet |
got rid of a pointer equality
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
tune the implementation of 'rel_coinduct'
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
generate 'rel_coinduct0' theorem for codatatypes
|
file |
diff |
annotate
|
| Thu, 08 May 2014 12:54:02 +0200 |
desharna |
note map_id0 more often
|
file |
diff |
annotate
|
| Thu, 08 May 2014 11:52:44 +0200 |
desharna |
generate 'map_ident' theorem for BNFs
|
file |
diff |
annotate
|
| Mon, 28 Apr 2014 00:54:30 +0200 |
blanchet |
more reliable 'name_of_bnf'
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 11:29:39 +0200 |
blanchet |
made SML/NJ happier
|
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:26 +0200 |
blanchet |
added 'inj_map' as auxiliary BNF theorem
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:17 +0200 |
kuncar |
revert idiomatic handling of namings from 5a93b8f928a2 because in combination with Named_Target.theory_init global names are sometimes created
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:16 +0200 |
kuncar |
don't forget to init Interpretation and transfer theorems in the interpretation hook
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 10:51:24 +0200 |
blanchet |
added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes
|
file |
diff |
annotate
|
| Tue, 01 Apr 2014 10:51:29 +0200 |
blanchet |
added BNF interpretation hook
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:23:16 +0100 |
traytel |
unfold intermediate definitions after sealing the bnf
|
file |
diff |
annotate
|