| Fri, 14 Aug 2020 14:40:24 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2019 11:12:55 +0100 |
wenzelm |
clarified modules;
|
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
|
| Fri, 23 Feb 2018 19:25:37 +0100 |
wenzelm |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
file |
diff |
annotate
|
| Thu, 11 Jan 2018 13:48:17 +0100 |
wenzelm |
uniform use of Standard ML op-infix -- eliminated warnings;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 26 Oct 2016 22:40:28 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 08 Sep 2016 10:35:08 +0200 |
blanchet |
made it easier to catch 'empty datatype' exception
|
file |
diff |
annotate
|
| Fri, 17 Jun 2016 21:00:32 +0200 |
blanchet |
killed deadcode
|
file |
diff |
annotate
|
| Thu, 02 Jun 2016 16:49:44 +0200 |
wenzelm |
eliminated pointless alias (no warning for duplicates);
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 20:29:42 +0200 |
traytel |
n2m operates on (un)folds
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 17:56:26 +0200 |
traytel |
(un)folds are not legacy
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 17:56:22 +0200 |
traytel |
derive (co)rec uniformly from (un)fold
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 09:54:17 +0200 |
traytel |
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
|
file |
diff |
annotate
|
| Sun, 03 Apr 2016 10:25:17 +0200 |
traytel |
tuned names
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
added '_legacy' suffixes
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 13:44:50 +0100 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 08:00:15 +0100 |
blanchet |
more debugging
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 07:18:36 +0100 |
traytel |
document that n2m does not depend on most things in fp_sugar in its type
|
file |
diff |
annotate
|
| Tue, 16 Feb 2016 22:28:19 +0100 |
traytel |
make predicator a first-class bnf citizen
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 12:01:07 +0200 |
traytel |
collect the names from goals in favor of fragile exports
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 23:01:34 +0200 |
traytel |
restructure fresh variable generation to make exports more wellformed
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 23:01:31 +0200 |
traytel |
more canonical context threading
|
file |
diff |
annotate
|
| Thu, 03 Sep 2015 16:41:43 +0200 |
traytel |
use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 17:24:54 +0200 |
wenzelm |
updated to infer_instantiate;
|
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
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:21:07 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2015 20:59:14 +0200 |
blanchet |
export more low-level theorems in data structure (partly for 'corec')
|
file |
diff |
annotate
|
| Thu, 26 Mar 2015 17:10:24 +0100 |
blanchet |
store low-level (un)fold constants
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 18:10:56 +0100 |
blanchet |
tuning
|
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
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 20:41:53 +0100 |
wenzelm |
proper proof context for typedef;
|
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
|
| Mon, 06 Oct 2014 13:41:37 +0200 |
desharna |
rename 'xtor_rel_thms' to 'xtor_rels'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:40:56 +0200 |
desharna |
rename 'xtor_set_thmss' to 'xtor_setss'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:40:31 +0200 |
desharna |
rename 'xtor_map_thms' to 'xtor_maps'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:39:12 +0200 |
desharna |
rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:38:40 +0200 |
desharna |
rename 'dtor_set_induct_thms' to 'dtor_set_inducts'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:38:13 +0200 |
desharna |
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:37:38 +0200 |
desharna |
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:56 +0200 |
desharna |
generate 'corec_transfer' for codatatypes
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:53 +0200 |
desharna |
generate 'rec_transfer' for datatypes
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:50 +0200 |
desharna |
generate 'ctor_rec_transfer' for datatypes
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 14:14:47 +0200 |
traytel |
goal generation for xtor_co_rec_transfer
|
file |
diff |
annotate
|
| Sat, 13 Sep 2014 18:08:38 +0200 |
blanchet |
imported patch phantoms
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:45:42 +0200 |
blanchet |
tuning terminology
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:41:45 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 23:09:24 +0200 |
blanchet |
tuned command descriptions
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 23:09:23 +0200 |
blanchet |
generate better internal names, with name of the target type in it
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
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
|
| Tue, 19 Aug 2014 09:34:30 +0200 |
blanchet |
don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
|
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
|
| Thu, 31 Jul 2014 13:19:57 +0200 |
traytel |
simplified tactics slightly
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 10:50:28 +0200 |
desharna |
generate 'set_induct' theorem for codatatypes
|
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
|
| Tue, 24 Jun 2014 15:49:20 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 26 May 2014 16:58:38 +0200 |
blanchet |
don't conceal (co)datatypes
|
file |
diff |
annotate
|
| Mon, 28 Apr 2014 00:54:30 +0200 |
blanchet |
more reliable 'name_of_bnf'
|
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 |
generate size instances for new-style datatypes
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 15:14:38 +0200 |
traytel |
more accurate type arguments for intermeadiate typedefs
|
file |
diff |
annotate
|
| Tue, 01 Apr 2014 11:02:40 +0200 |
traytel |
more precise BNF bound for datatypes
|
file |
diff |
annotate
|
| Tue, 01 Apr 2014 10:51:29 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 01 Apr 2014 10:51:29 +0200 |
blanchet |
added BNF interpretation hook
|
file |
diff |
annotate
|
| Tue, 01 Apr 2014 10:04:05 +0200 |
traytel |
tuned
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 13:14:33 +0100 |
traytel |
prove theorems with fixed variables (export afterwards)
|
file |
diff |
annotate
|
| Mon, 24 Mar 2014 16:33:36 +0100 |
traytel |
made tactic more robust
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 08:13:23 +0100 |
traytel |
simplified internal datatype construction
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 14:32:23 +0100 |
traytel |
changed policy when to define constants
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 16:28:25 +0100 |
traytel |
tuned tactics
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:23:16 +0100 |
traytel |
unfold intermediate definitions after sealing the bnf
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 18:57:17 +0100 |
blanchet |
renamed a pair of low-level theorems to have c/dtor in their names (like the others)
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 12:32:33 +0100 |
traytel |
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:19 +0100 |
blanchet |
optimize cardinal bounds involving natLeq (omega)
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 18:14:26 +0100 |
traytel |
joint work with blanchet: intermediate typedef for the input to fp-operations
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 23:09:29 +0100 |
traytel |
intermediate typedef for the type of the bound (local to lfp)
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:10:38 +0100 |
traytel |
made tactics more robust
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 22:51:11 +0100 |
blanchet |
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 14:51:26 +0100 |
traytel |
syntactic simplifications of internal (co)datatype constructions
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 18:18:27 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
tuning: moved code where it belongs
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 13:45:29 +0100 |
traytel |
register bnfs for (co)datatypes under their proper name (lost in af71b753c459)
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 12:16:59 +0100 |
traytel |
use Local_Theory.define instead of Specification.definition for internal constants
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:02:36 +0100 |
traytel |
less hermetic tactics
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
tuned names
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
adjusted comments
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
avoid nested 'Tools' directories
|
file |
diff |
annotate
| base
|