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
|