| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Wed, 17 Dec 2014 16:51:29 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 11:28:37 +0100 |
traytel |
more complete fp_sugars for sum and prod;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 11:52:54 +0100 |
desharna |
generate 'size_neq' for datatypes
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 17:23:14 +0200 |
desharna |
rename 'size_o_map' to 'size_gen_o_map'
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 17:23:13 +0200 |
desharna |
generate 'size_gen' for datatypes
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 17:23:12 +0200 |
desharna |
generate 'map_o_corec' for (co)datatypes
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 17:23:11 +0200 |
desharna |
move theorem 'rec_o_map'
|
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
|
| 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
|
| Fri, 26 Sep 2014 14:43:26 +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
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
moved old 'size' generator together with 'old_datatype'
|
file |
diff |
annotate
|
| Wed, 17 Sep 2014 08:24:10 +0200 |
blanchet |
syntactic check to determine when to prove 'nested_size_o_map'
|
file |
diff |
annotate
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
tuned fact visibility
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 11:37:55 +0200 |
blanchet |
tuned definition of 'size' function to get nicer properties
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 11:17:44 +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
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
pretend code generation is a ctr_sugar plugin
|
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 |
renamed internal constant
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
moved code around
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
tuned size function generation
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:34:40 +0200 |
blanchet |
renamed BNF theories
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 09:34:57 +0200 |
blanchet |
robustified tactics
|
file |
diff |
annotate
|
| Mon, 11 Aug 2014 10:43:03 +0200 |
traytel |
use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
|
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
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
tuned variable names
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
repaired BNF 'size' generation tactic for datatypes mixng old- and new-style datatypes on the right-hand side
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
tune the implementation of 'rel_coinduct'
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 11:59:51 +0200 |
blanchet |
removed some spurious warnings in new (co)datatype package
|
file |
diff |
annotate
|
| Thu, 15 May 2014 20:48:14 +0200 |
blanchet |
more aggressive nested size handling in the absence of 'size_o_map' theorems (+ unrelated pattern matching fix)
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 06:43:06 +0200 |
blanchet |
use right set of variables for recursive check
|
file |
diff |
annotate
|
| Fri, 25 Apr 2014 12:09:15 +0200 |
blanchet |
more unfolding and more folding in size equations, to look more natural in the nested case
|
file |
diff |
annotate
|
| Thu, 24 Apr 2014 21:00:00 +0200 |
blanchet |
really unfold
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
qualify name
|
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:27 +0200 |
blanchet |
no need to make 'size' generation an interpretation -- overkill
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
pick up all 'nesting' theorems
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
prevent tactic failures by detecting and ignoring BNFs with no 'size' functions early
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
move size hooks together, with new one preceding old one and sharing same theory data
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
allow registration of custom size functions for BNF-based datatypes
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
generate 'rec_o_map' and 'size_o_map' in size extension
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
generate size instances for new-style datatypes
|
file |
diff |
annotate
|