| #
026d96d6 |
|
02-Dec-2019 |
wenzelm <none@none> |
proper spec_rule name via naming/binding/Morphism.binding;
|
| #
44a31568 |
|
29-Nov-2019 |
wenzelm <none@none> |
more informative spec rules: optional name;
clarified signature;
more thorough treatment of Thm.trim_context vs. Thm.transfer;
|
| #
14c7fb8f |
|
09-Aug-2019 |
wenzelm <none@none> |
formal position for PThm nodes;
|
| #
d948ca9f |
|
26-Mar-2019 |
wenzelm <none@none> |
more informative Spec_Rules.Equational, notably primrec argument types;
|
| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
fcc9e542 |
|
23-Feb-2018 |
wenzelm <none@none> |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
| #
da18404a |
|
22-Feb-2018 |
wenzelm <none@none> |
tuned;
|
| #
9322bd71 |
|
02-Jul-2017 |
haftmann <none@none> |
proper concept of code declaration wrt. atomicity and Isar declarations
--HG--
extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472
|
| #
219bfdf8 |
|
22-Dec-2016 |
blanchet <none@none> |
generalized generation of coinduction goal (towards nonuniform codatatypes)
|
| #
eeeee96a |
|
22-Dec-2016 |
blanchet <none@none> |
export ML functions (towards nonuniform codatatypes) + signature tuning
|
| #
a972b36d |
|
20-Dec-2016 |
blanchet <none@none> |
generalized code (towards nonuniform datatypes)
|
| #
659a2dbd |
|
20-Dec-2016 |
blanchet <none@none> |
generalized ML function (towards nonuniform datatypes)
|
| #
8c45ffcd |
|
21-Dec-2016 |
blanchet <none@none> |
generalized ML function (towards nonuniform datatypes)
|
| #
b090623b |
|
21-Dec-2016 |
blanchet <none@none> |
renamed confusing variable names
|
| #
76ac1415 |
|
16-Dec-2016 |
blanchet <none@none> |
refactored induction principle generation code, for reuse for nonuniform datatypes
|
| #
3be1e856 |
|
27-Oct-2016 |
blanchet <none@none> |
tuning
|
| #
1df1830f |
|
27-Oct-2016 |
blanchet <none@none> |
more uniform treatment of codatatype vs. datatype map and rel theorem generation (towards nonuniform codatatypes)
|
| #
8aafd76b |
|
26-Oct-2016 |
blanchet <none@none> |
tuning
|
| #
2c388eb7 |
|
06-Oct-2016 |
traytel <none@none> |
less aggressive unfolding in tactic
|
| #
268559be |
|
13-Sep-2016 |
blanchet <none@none> |
union associates to the left
|
| #
d945085c |
|
12-Sep-2016 |
blanchet <none@none> |
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
|
| #
b77bce63 |
|
12-Sep-2016 |
blanchet <none@none> |
avoid warning triggered by code generator
|
| #
bd27a761 |
|
12-Sep-2016 |
blanchet <none@none> |
prove 'set' property backward
|
| #
63fa20eb |
|
11-Sep-2016 |
blanchet <none@none> |
generalized code towards nonuniform (co)datatypes
|
| #
e3d144da |
|
11-Sep-2016 |
blanchet <none@none> |
strengthened tactics
|
| #
a1eb81ce |
|
11-Sep-2016 |
blanchet <none@none> |
derive relator properties forward
|
| #
257f9e69 |
|
11-Sep-2016 |
blanchet <none@none> |
derive maps forward
|
| #
15e43059 |
|
11-Sep-2016 |
blanchet <none@none> |
tuning
|
| #
8c4c500b |
|
11-Sep-2016 |
blanchet <none@none> |
tuning
|
| #
14393da9 |
|
08-Sep-2016 |
blanchet <none@none> |
made it easier to catch 'empty datatype' exception
|
| #
da13635f |
|
08-Sep-2016 |
blanchet <none@none> |
export ML functions
|
| #
79f97a31 |
|
08-Sep-2016 |
blanchet <none@none> |
tuning
|
| #
f38f998e |
|
07-Sep-2016 |
blanchet <none@none> |
tuning
|
| #
2842edec |
|
07-Sep-2016 |
blanchet <none@none> |
exported ML functions + tuning
|
| #
baf09aac |
|
07-Sep-2016 |
blanchet <none@none> |
refactoring
|
| #
058469cf |
|
07-Sep-2016 |
blanchet <none@none> |
refactoring
|
| #
90c88247 |
|
07-Sep-2016 |
blanchet <none@none> |
refactoring
|
| #
dc32db36 |
|
07-Sep-2016 |
blanchet <none@none> |
tuned whitespace
|
| #
6750f4ae |
|
06-Sep-2016 |
blanchet <none@none> |
export more ML functions
|
| #
28ad8145 |
|
06-Sep-2016 |
blanchet <none@none> |
generalized ML signature
|
| #
25f52df5 |
|
06-Sep-2016 |
blanchet <none@none> |
tuned ML signature
|
| #
0e3f246a |
|
05-Sep-2016 |
blanchet <none@none> |
exported ML functions
|
| #
3d9861ee |
|
05-Sep-2016 |
blanchet <none@none> |
export ML function + tuning
|
| #
fa204375 |
|
05-Sep-2016 |
blanchet <none@none> |
export more ML functions
|
| #
104eba6e |
|
05-Sep-2016 |
blanchet <none@none> |
export more ML functions
|
| #
f02fe845 |
|
13-Aug-2016 |
blanchet <none@none> |
tuned ML
|
| #
2d2d3564 |
|
26-Jul-2016 |
traytel <none@none> |
honor sorts in (co)datatype declarations
|
| #
2e392e73 |
|
06-Jun-2016 |
haftmann <none@none> |
explicit tagging of code equations de-baroquifies interface
--HG--
extra : rebase_source : 1d83d31f669dc30b586df508a64fdc3a9e7b2655
|
| #
237f0cff |
|
02-Jun-2016 |
wenzelm <none@none> |
eliminated pointless alias (no warning for duplicates);
|
| #
d5d790a2 |
|
25-Apr-2016 |
blanchet <none@none> |
avoid duplicate mixfix messages in '(co)datatype' type name
|
| #
6bed86f1 |
|
18-Apr-2016 |
wenzelm <none@none> |
prefer internal attribute source;
|
| #
c4b0715f |
|
27-Mar-2016 |
blanchet <none@none> |
generalized ML function
|
| #
204828b6 |
|
27-Mar-2016 |
blanchet <none@none> |
generalized ML interface
|
| #
5851429c |
|
22-Mar-2016 |
blanchet <none@none> |
better warning, with definitions in right order
|
| #
4b4ae612 |
|
23-Feb-2016 |
blanchet <none@none> |
refactoring
|
| #
48f879b6 |
|
23-Feb-2016 |
blanchet <none@none> |
tuning
|
| #
11e3eaac |
|
23-Feb-2016 |
blanchet <none@none> |
tuning
|
| #
97b25dd9 |
|
17-Feb-2016 |
blanchet <none@none> |
making 'pred_inject' a first-class BNF citizen
|
| #
6b18406f |
|
16-Feb-2016 |
traytel <none@none> |
make predicator a first-class bnf citizen
|
| #
2971b896 |
|
15-Feb-2016 |
blanchet <none@none> |
tuning
|
| #
2514dd4c |
|
15-Feb-2016 |
blanchet <none@none> |
keep 'ctor_iff_dtor' theorem around in BNF FP database
|
| #
09941e1d |
|
14-Feb-2016 |
blanchet <none@none> |
tuning
|
| #
c13a38f2 |
|
13-Jan-2016 |
blanchet <none@none> |
generate stronger 'rel_(co)induct' and 'coinduct' principles for mutually (co)recursive (co)datatypes
|
| #
4216bc36 |
|
07-Jan-2016 |
wenzelm <none@none> |
more uniform treatment of package internals;
|
| #
591a7bfe |
|
01-Dec-2015 |
blanchet <none@none> |
tuned whitespace
|
| #
78e3cdc9 |
|
02-Nov-2015 |
blanchet <none@none> |
don't pollute local theory with needless names
|
| #
16fd80ec |
|
08-Oct-2015 |
blanchet <none@none> |
tuning
|
| #
b22e4c0f |
|
07-Oct-2015 |
blanchet <none@none> |
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
|
| #
0543912a |
|
06-Oct-2015 |
blanchet <none@none> |
avoid unsound 'nitpick_simp' attribute on nonterminating, nonproductive equations
|
| #
bcc1a605 |
|
06-Oct-2015 |
blanchet <none@none> |
generate 'case_transfer' unconditionally
|
| #
e5517855 |
|
05-Oct-2015 |
traytel <none@none> |
collect the names from goals in favor of fragile exports
|
| #
06b6c5f0 |
|
01-Oct-2015 |
blanchet <none@none> |
export '_cmd' functions
|
| #
6633bf2a |
|
23-Sep-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
13bb5ba7 |
|
22-Sep-2015 |
wenzelm <none@none> |
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
defs.ML: track dependencies also for type constructors;
typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type;
Pure types and typedecls are final -- no dependencies;
|
| #
1ae750a8 |
|
04-Sep-2015 |
wenzelm <none@none> |
close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;
|
| #
78d8b09f |
|
03-Sep-2015 |
traytel <none@none> |
use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
|
| #
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
839d9ae3 |
|
26-Jul-2015 |
wenzelm <none@none> |
updated to infer_instantiate;
|
| #
46ef1e1e |
|
16-Jul-2015 |
blanchet <none@none> |
tuning
|
| #
dbbe37ca |
|
15-Jul-2015 |
traytel <none@none> |
{r,e,d,f}tac with proper context in BNF
|
| #
00bb45b9 |
|
28-Apr-2015 |
blanchet <none@none> |
tuning
|
| #
f64d293f |
|
07-Apr-2015 |
blanchet <none@none> |
generalized slightly
|
| #
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
| #
b2fd0f75 |
|
31-Mar-2015 |
wenzelm <none@none> |
more standard Long_Name operations;
|
| #
03b64291 |
|
30-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
955d0fc8 |
|
26-Mar-2015 |
blanchet <none@none> |
store low-level (un)fold constants
|
| #
cd3872ba |
|
26-Mar-2015 |
blanchet <none@none> |
export more functions
|
| #
9113f38b |
|
24-Mar-2015 |
blanchet <none@none> |
tuning
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
b7bf58e6 |
|
03-Mar-2015 |
traytel <none@none> |
eliminated some clones of Proof_Context.cterm_of
|
| #
d9c8335a |
|
05-Jan-2015 |
blanchet <none@none> |
generate [code] only with 'code' plugin enabled
|
| #
ef71534e |
|
04-Jan-2015 |
blanchet <none@none> |
tuning
|
| #
07a7056b |
|
19-Dec-2014 |
desharna <none@none> |
Add plugin to generate transfer theorem for primrec and primcorec
|
| #
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
| #
ea5a3e95 |
|
10-Nov-2014 |
desharna <none@none> |
also generate '(co)rec_transfer' for (co)datatypes with 0 live type variables
|
| #
eb5e73fc |
|
11-Nov-2014 |
desharna <none@none> |
make 'rec_transfer' tactic more robust
|
| #
4eae0352 |
|
10-Nov-2014 |
wenzelm <none@none> |
proper context for assume_tac (atac remains as fall-back without context);
|
| #
c12ca051 |
|
07-Nov-2014 |
wenzelm <none@none> |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
|
| #
9dec7d71 |
|
06-Nov-2014 |
desharna <none@none> |
fix 'unfla' function
|
| #
824744a2 |
|
21-Oct-2014 |
desharna <none@none> |
generate 'map_o_corec' for (co)datatypes
* * *
document 'map_o_corec'
|
| #
686351a9 |
|
21-Oct-2014 |
desharna <none@none> |
move theorem 'rec_o_map'
* * *
move documentation of 'rec_o_map'
|
| #
f2bed2d2 |
|
21-Oct-2014 |
desharna <none@none> |
warn for not fully mutually (co)recursive types
|
| #
edebfbee |
|
16-Oct-2014 |
blanchet <none@none> |
made SML/NJ happier
|
| #
f05f85f5 |
|
14-Oct-2014 |
desharna <none@none> |
generate 'sel_transfer' for (co)datatypes
|
| #
8f51507f |
|
14-Oct-2014 |
desharna <none@none> |
add 'kind' to 'cr_sugar'
|
| #
5ae17a36 |
|
14-Oct-2014 |
desharna <none@none> |
add 'fp_bnf' to 'bnf_sugar'
|
| #
9c060c90 |
|
14-Oct-2014 |
desharna <none@none> |
preserve the structure of 'set_intros' theorem in ML
|
| #
def076b7 |
|
14-Oct-2014 |
desharna <none@none> |
preserve the structure of 'map_sel' theorem in ML
|
| #
2be8af88 |
|
14-Oct-2014 |
desharna <none@none> |
preserve the structure of 'set_sel' theorem in ML
|
| #
bb4c3636 |
|
13-Oct-2014 |
wenzelm <none@none> |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
| #
cbfdc100 |
|
08-Oct-2014 |
wenzelm <none@none> |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
| #
cbc989cb |
|
06-Oct-2014 |
desharna <none@none> |
refactor 'map_sel_thms' and 'set_sel_thms'
|
| #
9622cd51 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_rel_thms' to 'xtor_rels'
|
| #
191e6485 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_set_thmss' to 'xtor_setss'
|
| #
7d5fbd1c |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_map_thms' to 'xtor_maps'
|
| #
9b27f050 |
|
06-Oct-2014 |
desharna <none@none> |
rename one of the two 'rel_eq_thms' to 'rel_code_thms'
|
| #
57c1cff0 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
|
| #
c54f4f14 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'dtor_set_induct_thms' to 'dtor_set_inducts'
|
| #
9665b67b |
|
06-Oct-2014 |
desharna <none@none> |
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
|
| #
e364b08b |
|
06-Oct-2014 |
desharna <none@none> |
add 'set_inducts' to 'fp_sugar'
|
| #
2cedfc03 |
|
06-Oct-2014 |
desharna <none@none> |
add 'common_set_inducts' to 'fp_sugar'
|
| #
467db70c |
|
06-Oct-2014 |
desharna <none@none> |
add 'rel_co_inducts' to 'fp_sugar'
|
| #
cadb7741 |
|
06-Oct-2014 |
desharna <none@none> |
add 'common_rel_co_induct' to 'fp_sugar'
|
| #
d76bbcfd |
|
06-Oct-2014 |
desharna <none@none> |
add 'co_rec_transfers' to 'fp_sugar'
|
| #
6d76dc50 |
|
06-Oct-2014 |
desharna <none@none> |
add 'co_rec_disc_iffs' to 'fp_sugar'
|
| #
8b25f959 |
|
06-Oct-2014 |
desharna <none@none> |
add 'disc_transfers' to 'fp_sugar'
|
| #
b0fae040 |
|
06-Oct-2014 |
desharna <none@none> |
add 'case_transfers' to 'fp_sugar'
|
| #
3fbae9a8 |
|
06-Oct-2014 |
desharna <none@none> |
add 'ctr_transfers' to 'fp_sugar'
|
| #
f5c26cc0 |
|
06-Oct-2014 |
desharna <none@none> |
add 'set_cases' to 'fp_sugar'
|
| #
30cc7146 |
|
06-Oct-2014 |
desharna <none@none> |
add 'set_intros' to 'fp_sugar'
|
| #
b5244d83 |
|
06-Oct-2014 |
desharna <none@none> |
add 'set_sels' to 'fp_sugar'
|
| #
2ef889ae |
|
06-Oct-2014 |
desharna <none@none> |
add 'set_thms' to 'fp_sugar'
|
| #
3d17f9a3 |
|
06-Oct-2014 |
desharna <none@none> |
add 'rel_cases' to 'fp_sugar'
|
| #
58470965 |
|
06-Oct-2014 |
desharna <none@none> |
add 'rel_intros' to 'fp_sugar'
|
| #
24e3ec36 |
|
06-Oct-2014 |
desharna <none@none> |
add 'rel_sels' to 'fp_sugar'
|
| #
00bc7453 |
|
06-Oct-2014 |
desharna <none@none> |
add 'map_sels' to 'fp_sugar'
|
| #
4a7808d9 |
|
06-Oct-2014 |
desharna <none@none> |
add 'map_disc_iffs' to 'fp_sugar'
|
| #
5bbf7250 |
|
01-Oct-2014 |
blanchet <none@none> |
tuning
|
| #
669d9d3b |
|
29-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
906e82c7 |
|
26-Sep-2014 |
desharna <none@none> |
refactor fp_sugar move theorems
|
| #
4434c5ed |
|
26-Sep-2014 |
desharna <none@none> |
refactor fp_sugar move theorems
|
| #
9608121d |
|
26-Sep-2014 |
desharna <none@none> |
refactor fp_sugar move theorems
|
| #
a14f7fdb |
|
26-Sep-2014 |
desharna <none@none> |
refactor fp_sugar move theorems
|
| #
aa3cb8c8 |
|
26-Sep-2014 |
desharna <none@none> |
refactor fp_sugar move theorems
|
| #
50b15776 |
|
26-Sep-2014 |
desharna <none@none> |
refactor fp_sugar with empty substructures
|
| #
1049fe9a |
|
26-Sep-2014 |
desharna <none@none> |
add attribute 'case_names' to 'set_case'
|
| #
eb1ed55c |
|
25-Sep-2014 |
desharna <none@none> |
generate 'corec_transfer' for codatatypes
|
| #
e05be41f |
|
25-Sep-2014 |
desharna <none@none> |
generate 'rec_transfer' for datatypes
|
| #
95e3c694 |
|
24-Sep-2014 |
blanchet <none@none> |
avoid type variable name clash
|
| #
28df263f |
|
24-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
997718be |
|
16-Sep-2014 |
blanchet <none@none> |
register 'prod' and 'sum' as datatypes, to allow N2M through them
|
| #
b372934b |
|
15-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
080b92c6 |
|
15-Sep-2014 |
blanchet <none@none> |
refactoring
|
| #
65642a5b |
|
15-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
2a9622ce |
|
15-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
6b777fb4 |
|
15-Sep-2014 |
blanchet <none@none> |
generate 'code' attribute only if 'code' plugin is enabled
|
| #
22f3dd87 |
|
13-Sep-2014 |
blanchet <none@none> |
imported patch phantoms
|
| #
c1cf7621 |
|
12-Sep-2014 |
desharna <none@none> |
refactor repeated terms in a single variable
|
| #
10742fde |
|
12-Sep-2014 |
desharna <none@none> |
make 'ctr_transfer' tactic more robust
|
| #
bbf13194 |
|
12-Sep-2014 |
desharna <none@none> |
make 'rel_sel' and 'map_sel' tactics more robust
|
| #
9a4a064f |
|
09-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
a61a03aa |
|
09-Sep-2014 |
blanchet <none@none> |
avoid duplicate case names
|
| #
abf5628f |
|
09-Sep-2014 |
blanchet <none@none> |
nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')
|
| #
02b2c624 |
|
09-Sep-2014 |
blanchet <none@none> |
preserve case names in '(co)induct' theorems generated by prim(co)rec'
|
| #
fd6861bc |
|
09-Sep-2014 |
blanchet <none@none> |
set 'fundef_cong' attribute also for (co)datatypes with no live type variables
|
| #
127f3858 |
|
09-Sep-2014 |
blanchet <none@none> |
prevent infinite loop when type variables are of a non-'type' sort
|
| #
377145ae |
|
09-Sep-2014 |
blanchet <none@none> |
tuned code
|
| #
dab46d6b |
|
08-Sep-2014 |
blanchet <none@none> |
honour sorts in N2M
|
| #
eb8f2765 |
|
08-Sep-2014 |
blanchet <none@none> |
proper sort constraints in map and rel theorems
|
| #
d29de8b4 |
|
08-Sep-2014 |
blanchet <none@none> |
made code work also in the presence of deads
|
| #
53dc3f8b |
|
08-Sep-2014 |
blanchet <none@none> |
properly note theorems for split recursors
|
| #
75fd5395 |
|
08-Sep-2014 |
blanchet <none@none> |
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
|
| #
9fd98ddb |
|
08-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
427172cf |
|
08-Sep-2014 |
blanchet <none@none> |
export one more ML function
|
| #
241c5b8f |
|
08-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
6bd76c01 |
|
04-Sep-2014 |
blanchet <none@none> |
pretend code generation is a ctr_sugar plugin
|
| #
cc5256c1 |
|
04-Sep-2014 |
blanchet <none@none> |
added 'plugins' option to control which hooks are enabled
|
| #
c11a8aa4 |
|
04-Sep-2014 |
blanchet <none@none> |
introduced mechanism to filter interpretations
|
| #
d36b3fcf |
|
04-Sep-2014 |
blanchet <none@none> |
fixed infinite loops in 'register' functions + more uniform API
|
| #
625d35eb |
|
04-Sep-2014 |
blanchet <none@none> |
named interpretations
|
| #
21ec0eae |
|
04-Sep-2014 |
blanchet <none@none> |
centralized and cleaned up naming handling
|
| #
a030c224 |
|
04-Sep-2014 |
blanchet <none@none> |
tweaked setup for datatype realizer
|
| #
f4f86474 |
|
04-Sep-2014 |
blanchet <none@none> |
moved code around
|
| #
ec4e6125 |
|
04-Sep-2014 |
blanchet <none@none> |
tuned size function generation
|
| #
3a5bbb8e |
|
03-Sep-2014 |
blanchet <none@none> |
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
|
| #
87a971e8 |
|
03-Sep-2014 |
blanchet <none@none> |
tuned BNF database handling
|
| #
0a4b950c |
|
02-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
9c861e3b |
|
01-Sep-2014 |
blanchet <none@none> |
more compatibility between old- and new-style datatypes
|
| #
812558c3 |
|
01-Sep-2014 |
blanchet <none@none> |
added theory-based getters for convenience
|
| #
978db45e |
|
01-Sep-2014 |
blanchet <none@none> |
made transfer functions slightly more general
|
| #
fb2f6a3a |
|
01-Sep-2014 |
blanchet <none@none> |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
--HG--
rename : src/HOL/Datatype.thy => src/HOL/Old_Datatype.thy
rename : src/HOL/Tools/Function/size.ML => src/HOL/Tools/Function/old_size.ML
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Old_Datatype/old_datatype.ML
rename : src/HOL/Tools/Datatype/datatype_aux.ML => src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
rename : src/HOL/Tools/Datatype/datatype_codegen.ML => src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML
rename : src/HOL/Tools/Datatype/datatype_data.ML => src/HOL/Tools/Old_Datatype/old_datatype_data.ML
rename : src/HOL/Tools/Datatype/datatype_prop.ML => src/HOL/Tools/Old_Datatype/old_datatype_prop.ML
rename : src/HOL/Tools/Datatype/datatype_realizer.ML => src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML
rename : src/HOL/Tools/Datatype/primrec.ML => src/HOL/Tools/Old_Datatype/old_primrec.ML
rename : src/HOL/Tools/Datatype/rep_datatype.ML => src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
|
| #
439a0059 |
|
01-Sep-2014 |
desharna <none@none> |
generate 'rel_transfer' for BNFs
|
| #
7666c0e4 |
|
29-Aug-2014 |
desharna <none@none> |
generate 'disc_transfer' for (co)datatypes
|
| #
dffb56b9 |
|
29-Aug-2014 |
desharna <none@none> |
generate 'case_transfer' for (co)datatypes
|
| #
c810fc8c |
|
27-Aug-2014 |
blanchet <none@none> |
removed not so interesting 'set_empty'
|
| #
d65030e5 |
|
19-Aug-2014 |
wenzelm <none@none> |
tuned signature -- moved type src to Token, without aliases;
|
| #
61a0a307 |
|
19-Aug-2014 |
desharna <none@none> |
generate 'ctr_transfer' for (co)datatypes
|
| #
3aeea22d |
|
18-Aug-2014 |
blanchet <none@none> |
set attributes on 'set_cases' theorem
|
| #
6fb4e52a |
|
18-Aug-2014 |
blanchet <none@none> |
reordered some (co)datatype property names for more consistency
|
| #
173fde0a |
|
14-Aug-2014 |
desharna <none@none> |
generate 'rel_map' theorem for BNFs
|
| #
0d4c8935 |
|
12-Aug-2014 |
blanchet <none@none> |
avoid needless (and wrong w.r.t. sorts) generation of type variables; tuned whitespaces;
|
| #
31574ff5 |
|
11-Aug-2014 |
desharna <none@none> |
generate 'set_cases' theorem for (co)datatypes
|
| #
534babeb |
|
11-Aug-2014 |
desharna <none@none> |
generate 'set_intros' theorem for (co)datatypes
|
| #
ef2d5221 |
|
11-Aug-2014 |
traytel <none@none> |
use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
|
| #
c96acc61 |
|
06-Aug-2014 |
blanchet <none@none> |
generate nicer 'set' theorems for (co)datatypes
|
| #
33c09681 |
|
30-Jul-2014 |
blanchet <none@none> |
correctly resolve selector names in default value equations
|
| #
a1b49062 |
|
27-Jul-2014 |
desharna <none@none> |
made tactic more robust w.r.t. dead variables; tuned;
|
| #
7b8e65c1 |
|
25-Jul-2014 |
blanchet <none@none> |
tuning
|
| #
657102e8 |
|
24-Jul-2014 |
blanchet <none@none> |
tuned code
|
| #
8c308eea |
|
23-Jul-2014 |
blanchet <none@none> |
repaired named derivations
|
| #
97fe0137 |
|
23-Jul-2014 |
blanchet <none@none> |
use the noted theorem whenever possible, also in 'BNF_Def'
|
| #
8f9d0c84 |
|
17-Jul-2014 |
desharna <none@none> |
fix bug caused by bad context
|
| #
efd75a1e |
|
17-Jul-2014 |
desharna <none@none> |
add mk_Trueprop_mem utility function
|
| #
2b38c5f0 |
|
16-Jul-2014 |
desharna <none@none> |
refactor commonly used functions
|
| #
0352f504 |
|
16-Jul-2014 |
desharna <none@none> |
generate 'rel_sel' theorem for (co)datatypes
|
| #
e1bd1185 |
|
16-Jul-2014 |
desharna <none@none> |
fix rel_cases
|
| #
3d51a59e |
|
14-Jul-2014 |
blanchet <none@none> |
took out 'rel_cases' for now because of failing tactic
|
| #
0bbf7ec1 |
|
09-Jul-2014 |
blanchet <none@none> |
made SML/NJ happier
|
| #
793f1234 |
|
07-Jul-2014 |
desharna <none@none> |
generate 'rel_cases' theorem for (co)datatypes
|
| #
109d7354 |
|
03-Jul-2014 |
desharna <none@none> |
generate 'rel_intros' theorem for (co)datatypes
|
| #
34b0a47c |
|
02-Jul-2014 |
desharna <none@none> |
generate 'corec_code' theorem for codatatypes
|
| #
c335096a |
|
01-Jul-2014 |
desharna <none@none> |
generate 'rel_induct' theorem for datatypes
|
| #
c1bd04e5 |
|
27-Jun-2014 |
blanchet <none@none> |
compile
|
| #
6f5ea271 |
|
27-Jun-2014 |
blanchet <none@none> |
tuned variable names
|
| #
7bbce892 |
|
30-Jul-2014 |
desharna <none@none> |
generate 'set_induct' theorem for codatatypes
|
| #
020ff44f |
|
24-Jun-2014 |
desharna <none@none> |
tune the implementation of 'rel_coinduct'
|
| #
104e77f3 |
|
24-Jun-2014 |
desharna <none@none> |
generate 'rel_coinduct' theorem for codatatypes
|
| #
a0ad2713 |
|
24-Jun-2014 |
desharna <none@none> |
generate 'rel_coinduct0' theorem for codatatypes
|
| #
7c886e63 |
|
18-Jun-2014 |
blanchet <none@none> |
made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
|
| #
1ddd04cf |
|
16-Jun-2014 |
blanchet <none@none> |
fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
|
| #
42cd340d |
|
10-Jun-2014 |
blanchet <none@none> |
changed syntax of map: and rel: arguments to BNF-based datatypes
|
| #
ce4b8eee |
|
10-Jun-2014 |
blanchet <none@none> |
tuning
|
| #
ed20523b |
|
09-Jun-2014 |
blanchet <none@none> |
use 'where' clause for selector default value syntax
|
| #
cca982c5 |
|
10-Jun-2014 |
blanchet <none@none> |
tuning
|
| #
112d96ec |
|
02-Jun-2014 |
desharna <none@none> |
generate 'sel_set' theorem for (co)datatypes
|
| #
517cc9da |
|
27-May-2014 |
blanchet <none@none> |
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
|
| #
312f030c |
|
26-May-2014 |
blanchet <none@none> |
got rid of '=:' squiggly
|
| #
440f2078 |
|
21-May-2014 |
desharna <none@none> |
generate 'sel_map[simp]' theorem for (co)datatypes and tuning 'disc_map_iff'
|
| #
d90e6fd8 |
|
15-May-2014 |
desharna <none@none> |
generate 'disc_map_iff[simp]' theorem for (co)datatypes
|
| #
2b30935a |
|
15-May-2014 |
blanchet <none@none> |
proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all low-level constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')
|
| #
09078cfa |
|
12-May-2014 |
desharna <none@none> |
generate 'set_empty' theorem for BNFs
|
| #
9e80e60b |
|
27-Apr-2014 |
blanchet <none@none> |
restored naming trick
|
| #
1c1981c6 |
|
27-Apr-2014 |
blanchet <none@none> |
cleaner 'rel_inject' theorems
|
| #
7369466c |
|
23-Apr-2014 |
blanchet <none@none> |
made SML/NJ happier
|
| #
aea2cf85 |
|
23-Apr-2014 |
blanchet <none@none> |
localize new size function generation code
|
| #
ebf08b80 |
|
23-Apr-2014 |
blanchet <none@none> |
no need to make 'size' generation an interpretation -- overkill
|
| #
173cad60 |
|
23-Apr-2014 |
blanchet <none@none> |
manual merge + added 'rel_distincts' field to record for symmetry
|
| #
90e83a10 |
|
23-Apr-2014 |
blanchet <none@none> |
reverted rb458558cbcc2 -- better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the low-level recursor) and 'rec'
|
| #
72596a3c |
|
23-Apr-2014 |
blanchet <none@none> |
generate 'rec_o_map' and 'size_o_map' in size extension
|
| #
df15a7e7 |
|
23-Apr-2014 |
blanchet <none@none> |
generate size instances for new-style datatypes
|
| #
b915e4a4 |
|
23-Apr-2014 |
blanchet <none@none> |
invoke 'fp_sugar' interpretation hook on mutually recursive clique
|
| #
88c45359 |
|
10-Apr-2014 |
kuncar <none@none> |
revert idiomatic handling of namings from 5a93b8f928a2 because in combination with Named_Target.theory_init global names are sometimes created
|
| #
6a76ebd9 |
|
10-Apr-2014 |
kuncar <none@none> |
don't forget to init Interpretation and transfer theorems in the interpretation hook
|
| #
8d0ad389 |
|
10-Apr-2014 |
kuncar <none@none> |
export theorems
|
| #
e0a8605f |
|
03-Apr-2014 |
blanchet <none@none> |
added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes
|
| #
19e8f7ca |
|
01-Apr-2014 |
blanchet <none@none> |
added new-style (co)datatype interpretation hook
|
| #
3c4f4261 |
|
22-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
| #
360c732d |
|
11-Mar-2014 |
blanchet <none@none> |
added missing theorems to unfolding set
|
| #
147d4ad6 |
|
07-Mar-2014 |
blanchet <none@none> |
tuning
|
| #
d815b696 |
|
06-Mar-2014 |
blanchet <none@none> |
balance tuples that represent curried functions
|
| #
11682cfd |
|
04-Mar-2014 |
blanchet <none@none> |
register relator equations as spec rules only for datatypes -- for codatatypes they underspecify the function and are therefore dangerous (e.g. to Nitpick)
|
| #
908441e2 |
|
04-Mar-2014 |
blanchet <none@none> |
renamed a pair of low-level theorems to have c/dtor in their names (like the others)
|
| #
35d9dd12 |
|
02-Mar-2014 |
blanchet <none@none> |
removed (co)iterators from documentation
|
| #
c39b02f9 |
|
02-Mar-2014 |
blanchet <none@none> |
rationalized internals
|
| #
5f1d2990 |
|
02-Mar-2014 |
blanchet <none@none> |
rationalized internals
|
| #
a350d601 |
|
02-Mar-2014 |
blanchet <none@none> |
rationalized internals
|
| #
da5d3a70 |
|
02-Mar-2014 |
blanchet <none@none> |
rationalized internals
|
| #
2e7739d0 |
|
02-Mar-2014 |
blanchet <none@none> |
rationalized internals
|
| #
b29ffe0e |
|
02-Mar-2014 |
blanchet <none@none> |
rationalize internals
|
| #
6c7be66c |
|
02-Mar-2014 |
blanchet <none@none> |
optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant
|
| #
9c62b91a |
|
02-Mar-2014 |
blanchet <none@none> |
compile
|
| #
209f60a6 |
|
02-Mar-2014 |
blanchet <none@none> |
repaired argument list to corecursor
|
| #
a3a1f899 |
|
02-Mar-2014 |
blanchet <none@none> |
got rid of automatically generated fold constant and theorems (to reduce overhead)
|
| #
dd1a06aa |
|
25-Feb-2014 |
traytel <none@none> |
joint work with blanchet: intermediate typedef for the input to fp-operations
|
| #
ae64540a |
|
27-Feb-2014 |
blanchet <none@none> |
correct most general type for mutual recursion when several identical types are involved
|
| #
2f1f0a53 |
|
23-Feb-2014 |
blanchet <none@none> |
added explicit killing
|
| #
6b413446 |
|
23-Feb-2014 |
blanchet <none@none> |
more precise error message
|
| #
dec58eb7 |
|
23-Feb-2014 |
blanchet <none@none> |
reuse same parser for '(co)datatype(_new)' as for 'bnf_decl'
|
| #
04523a1c |
|
19-Feb-2014 |
blanchet <none@none> |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
| #
1770bd13 |
|
19-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
efebaf05 |
|
18-Feb-2014 |
blanchet <none@none> |
prepare two-stage 'primrec' setup
|
| #
e9c8b8d7 |
|
18-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
8d680255 |
|
17-Feb-2014 |
blanchet <none@none> |
simplified data structure by reducing the incidence of clumsy indices
|
| #
99807201 |
|
17-Feb-2014 |
blanchet <none@none> |
name derivations in 'primrec' for code extraction from proof terms
|
| #
2f309df2 |
|
14-Feb-2014 |
blanchet <none@none> |
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
|
| #
dabb17d7 |
|
14-Feb-2014 |
blanchet <none@none> |
tuned code to allow mutualized corecursion through different functions with the same target type
|
| #
0ba161cf |
|
14-Feb-2014 |
blanchet <none@none> |
allow different functions to recurse on the same type, like in the old package
|
| #
2da87f73 |
|
13-Feb-2014 |
blanchet <none@none> |
more precise spec rules for selectors
|
| #
8e6ecc59 |
|
13-Feb-2014 |
blanchet <none@none> |
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
|
| #
1ae6608b |
|
13-Feb-2014 |
blanchet <none@none> |
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
|
| #
df2193a1 |
|
13-Feb-2014 |
blanchet <none@none> |
register 'Spec_Rules' for new-style (co)datatypes
|
| #
f8a77a2c |
|
12-Feb-2014 |
blanchet <none@none> |
iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
|
| #
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
| #
dea2cf15 |
|
12-Feb-2014 |
blanchet <none@none> |
killed 'rep_compat' option
|
| #
fff4f229 |
|
12-Feb-2014 |
blanchet <none@none> |
made 'ctr_sugar' more friendly to the 'datatype_realizer'
* * *
reverted changes to 'datatype_realizer.ML'
|
| #
2e6f9ae6 |
|
12-Feb-2014 |
blanchet <none@none> |
generate 'fundec_cong' attribute for new-style (co)datatypes
* * *
compile
|
| #
34f4cd23 |
|
12-Feb-2014 |
blanchet <none@none> |
more liberal merging of BNFs and constructor sugar
* * *
make sure that the cache doesn't produce 'DUP's
|
| #
d45839cf |
|
07-Feb-2014 |
blanchet <none@none> |
reverted a87e49f4336d -- overwriting of data entries yields to merge problems later
|
| #
0333edae |
|
06-Feb-2014 |
blanchet <none@none> |
allow multiple registration of the same type, the last wins
|
| #
c0de7553 |
|
05-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
a054fc0f |
|
21-Jan-2014 |
blanchet <none@none> |
made SML/NJ happier
|
| #
06fce64d |
|
21-Jan-2014 |
blanchet <none@none> |
made SML/NJ happier
|
| #
e6c141bc |
|
20-Jan-2014 |
blanchet <none@none> |
removed dependency of BNF package on Nitpick
|
| #
e8e169dd |
|
20-Jan-2014 |
blanchet <none@none> |
adjusted comments
|
| #
a0868967 |
|
20-Jan-2014 |
blanchet <none@none> |
avoid nested 'Tools' directories
--HG--
rename : src/HOL/Tools/BNF/Tools/bnf_comp.ML => src/HOL/Tools/BNF/bnf_comp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_comp_tactics.ML => src/HOL/Tools/BNF/bnf_comp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_def.ML => src/HOL/Tools/BNF/bnf_def.ML
rename : src/HOL/Tools/BNF/Tools/bnf_def_tactics.ML => src/HOL/Tools/BNF/bnf_def_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_def_sugar.ML => src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_def_sugar_tactics.ML => src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m.ML => src/HOL/Tools/BNF/bnf_fp_n2m.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m_sugar.ML => src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m_tactics.ML => src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_rec_sugar_util.ML => src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_util.ML => src/HOL/Tools/BNF/bnf_fp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp.ML => src/HOL/Tools/BNF/bnf_gfp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_rec_sugar.ML => src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML => src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_tactics.ML => src/HOL/Tools/BNF/bnf_gfp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_util.ML => src/HOL/Tools/BNF/bnf_gfp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp.ML => src/HOL/Tools/BNF/bnf_lfp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_compat.ML => src/HOL/Tools/BNF/bnf_lfp_compat.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_rec_sugar.ML => src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_tactics.ML => src/HOL/Tools/BNF/bnf_lfp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_util.ML => src/HOL/Tools/BNF/bnf_lfp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_tactics.ML => src/HOL/Tools/BNF/bnf_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_util.ML => src/HOL/Tools/BNF/bnf_util.ML
|