| 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
|
| Fri, 17 Jun 2016 21:35:35 +0200 |
blanchet |
killed dead code
|
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 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, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
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, 24 Sep 2015 12:28:15 +0200 |
traytel |
congruence rules for the relator
|
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
|
| 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:51 +0200 |
desharna |
generate 'dtor_corec_transfer' for codatatypes
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 14:14:47 +0200 |
traytel |
goal generation for xtor_co_rec_transfer
|
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: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
|
| 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
|
| 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
|
| Thu, 10 Apr 2014 15:14:38 +0200 |
traytel |
more accurate type arguments for intermeadiate typedefs
|
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, 25 Mar 2014 13:14:33 +0100 |
traytel |
prove theorems with fixed variables (export afterwards)
|
file |
diff |
annotate
|
| Mon, 17 Mar 2014 17:35:39 +0100 |
traytel |
tuned internal construction
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 16:28:25 +0100 |
traytel |
tuned tactics
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 11:15:04 +0100 |
traytel |
simplified internal codatatype construction
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 14:46:22 +0100 |
traytel |
tuned tactic
|
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
|
| Tue, 04 Mar 2014 09:29:56 +0100 |
blanchet |
removed debugging leftover
|
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
|
| Fri, 21 Feb 2014 12:33:49 +0100 |
traytel |
only one internal coinduction rule
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 11:40:03 +0100 |
traytel |
made tactics more robust
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 12:04:21 +0100 |
traytel |
another simplification of internal codatatype construction
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 09:50:50 +0100 |
traytel |
simplifications of internal codatatype construction
|
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
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
adapted theories to 'xxx_case' to 'case_xxx'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
adapted theories to '{case,rec}_{list,option}' names
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
|
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 |
made BNF compile after move to HOL
|
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
|