| #
cf411881 |
|
28-Feb-2020 |
traytel <none@none> |
tuned lift_bnf's user interface for quotients
|
| #
043c3b16 |
|
18-Jan-2020 |
traytel <none@none> |
new examples of BNF lifting across quotients using a new theory of confluence,
which simplifies the relator subdistributivity proof obligation
(a few new useful notions were added to HOL;
notably the symmetric and equivalence closures of a relation)
|
| #
3d6494dc |
|
07-Jan-2020 |
traytel <none@none> |
eliminated one redundant proof obligation in lift_bnf for quotients
|
| #
68eef6b5 |
|
09-Dec-2019 |
traytel <none@none> |
NEWS, CONTRIBUTORS, and documentation
|
| #
c277634b |
|
11-Oct-2019 |
blanchet <none@none> |
document antiquotations + clarify porting text slightly
|
| #
a3f9e217 |
|
10-Oct-2019 |
blanchet <none@none> |
added para constrasting 'primrec' and 'fun' -- and removed my middle name
|
| #
308e26bd |
|
07-Apr-2019 |
traytel <none@none> |
bundle for cardinal syntax
|
| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
f2d8c31b |
|
26-Dec-2018 |
wenzelm <none@none> |
isabelle update_cartouches -t;
|
| #
8413f38b |
|
22-Jun-2018 |
wenzelm <none@none> |
clarified document antiquotation @{theory};
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
f8a170c4 |
|
02-Jan-2018 |
blanchet <none@none> |
removed para about 'old_datatype' in docs
|
| #
4fa031b8 |
|
02-Jan-2018 |
wenzelm <none@none> |
old_datatype no longer exists (cf. 706b1cf7b76d);
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
682c20ef |
|
23-Jan-2017 |
traytel <none@none> |
tuned documentation
|
| #
9b9c2176 |
|
12-Aug-2016 |
wenzelm <none@none> |
more symbols;
|
| #
37b50607 |
|
11-Aug-2016 |
wenzelm <none@none> |
clarified antiquotations;
|
| #
5dc803d8 |
|
13-Apr-2016 |
wenzelm <none@none> |
eliminated "xname" and variants;
|
| #
a60bb699 |
|
30-Mar-2016 |
blanchet <none@none> |
more 'corec' docs
|
| #
d0408ac4 |
|
29-Mar-2016 |
blanchet <none@none> |
more 'corec' docs
|
| #
40e67883 |
|
29-Mar-2016 |
blanchet <none@none> |
tuning
|
| #
2111cf75 |
|
27-Mar-2016 |
blanchet <none@none> |
tuning
|
| #
3e14aa83 |
|
23-Feb-2016 |
blanchet <none@none> |
updated doc
|
| #
c19760ce |
|
17-Feb-2016 |
blanchet <none@none> |
tuning
|
| #
da6ae37f |
|
17-Feb-2016 |
traytel <none@none> |
adjust 112eefe85ff0 to 532ad8de5d61
|
| #
1df81bb7 |
|
17-Feb-2016 |
traytel <none@none> |
correct (apparently untested) e1698a9578ea
|
| #
34aef695 |
|
17-Feb-2016 |
traytel <none@none> |
document predicator in datatypes
|
| #
ef2cc6c5 |
|
17-Feb-2016 |
traytel <none@none> |
call the predicator of list list_all
|
| #
8cd1ee97 |
|
16-Feb-2016 |
blanchet <none@none> |
document new 'primrec' feature
|
| #
6b18406f |
|
16-Feb-2016 |
traytel <none@none> |
make predicator a first-class bnf citizen
|
| #
d96c62ea |
|
14-Feb-2016 |
blanchet <none@none> |
document a limitation of 'primcorec'
|
| #
4216bc36 |
|
07-Jan-2016 |
wenzelm <none@none> |
more uniform treatment of package internals;
|
| #
3cd59c15 |
|
06-Jan-2016 |
blanchet <none@none> |
updated docs
|
| #
1d301e19 |
|
04-Dec-2015 |
blanchet <none@none> |
tuned docs
|
| #
4d885b36 |
|
04-Dec-2015 |
blanchet <none@none> |
more documentation on 'size' plugin
|
| #
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
| #
35815136 |
|
07-Oct-2015 |
blanchet <none@none> |
clarify docs
|
| #
462a6ec2 |
|
07-Oct-2015 |
blanchet <none@none> |
updated docs
|
| #
c012b223 |
|
07-Oct-2015 |
blanchet <none@none> |
made documentation more accurate
|
| #
b7bc95db |
|
01-Oct-2015 |
blanchet <none@none> |
tuned documentation
|
| #
5bd5a3c8 |
|
01-Oct-2015 |
blanchet <none@none> |
tuned datatype docs
|
| #
9ec94e1d |
|
23-Sep-2015 |
traytel <none@none> |
congruence rules for the relator
|
| #
3349054e |
|
23-Sep-2015 |
traytel <none@none> |
more useful properties of the relators
|
| #
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
| #
93f0bd28 |
|
12-Aug-2015 |
traytel <none@none> |
NEWS, CONTRIBUTORS, documentation for lift_bnf
|
| #
ad597715 |
|
16-Jul-2015 |
blanchet <none@none> |
generalized limitation in documentation
|
| #
39301436 |
|
06-May-2015 |
blanchet <none@none> |
added acknowledgment
|
| #
197dc8f4 |
|
06-May-2015 |
blanchet <none@none> |
corrected path in doc
|
| #
00bb45b9 |
|
28-Apr-2015 |
blanchet <none@none> |
tuning
|
| #
0bb05f41 |
|
22-Apr-2015 |
blanchet <none@none> |
improved docs
|
| #
36cfd27e |
|
19-Apr-2015 |
blanchet <none@none> |
acknowledgment
|
| #
736b56ce |
|
19-Apr-2015 |
blanchet <none@none> |
suppressed warnings
|
| #
44d833b9 |
|
19-Apr-2015 |
blanchet <none@none> |
updated docs, esp. relating to 'datatype_compat'
|
| #
bfdc6fca |
|
19-Apr-2015 |
kleing <none@none> |
typo
|
| #
04a550b9 |
|
31-Mar-2015 |
blanchet <none@none> |
tuned doc
|
| #
897af4da |
|
27-Mar-2015 |
blanchet <none@none> |
clarified doc
|
| #
f46456ff |
|
24-Mar-2015 |
blanchet <none@none> |
reordered properties
|
| #
ed3b42b8 |
|
16-Mar-2015 |
traytel <none@none> |
document property
|
| #
41635d12 |
|
16-Mar-2015 |
blanchet <none@none> |
updated docs
|
| #
9161025c |
|
16-Mar-2015 |
blanchet <none@none> |
clarified documentation
|
| #
b93f8b2d |
|
03-Mar-2015 |
blanchet <none@none> |
updated docs
|
| #
dd3e187b |
|
06-Jan-2015 |
blanchet <none@none> |
docs
|
| #
92dbbb51 |
|
06-Jan-2015 |
blanchet <none@none> |
docs
|
| #
1997421f |
|
06-Jan-2015 |
blanchet <none@none> |
docs
|
| #
cf136718 |
|
05-Jan-2015 |
blanchet <none@none> |
docs
|
| #
d281c253 |
|
05-Jan-2015 |
blanchet <none@none> |
docs
|
| #
5183ba84 |
|
05-Jan-2015 |
blanchet <none@none> |
docs
|
| #
69302b29 |
|
05-Jan-2015 |
blanchet <none@none> |
docs
|
| #
24b2cc8e |
|
04-Jan-2015 |
blanchet <none@none> |
documented 'transfer' options to 'prim(co)rec'
|
| #
b7279d90 |
|
19-Dec-2014 |
desharna <none@none> |
document 'disc_eq_case'
|
| #
cb86d016 |
|
19-Dec-2014 |
desharna <none@none> |
document 'case_distrib'
|
| #
77707fbe |
|
22-Apr-2015 |
blanchet <none@none> |
doc
|
| #
63440213 |
|
07-Nov-2014 |
wenzelm <none@none> |
clarified keyword categories;
tuned;
|
| #
ba55a16a |
|
06-Nov-2014 |
desharna <none@none> |
document '*_transfer' attribute
|
| #
39c5008a |
|
07-Nov-2014 |
desharna <none@none> |
document 'size_neq'
|
| #
f6df0208 |
|
21-Oct-2014 |
desharna <none@none> |
update documentation for 'size_o_map'
|
| #
225cdcb4 |
|
21-Oct-2014 |
desharna <none@none> |
document 'size_gen'
|
| #
3ffef250 |
|
21-Oct-2014 |
desharna <none@none> |
document 'map_o_corec'
|
| #
25c0ab33 |
|
21-Oct-2014 |
desharna <none@none> |
move documentation of 'rec_o_map'
|
| #
24df2722 |
|
14-Oct-2014 |
desharna <none@none> |
document 'sel_transfer'
|
| #
bb4c3636 |
|
13-Oct-2014 |
wenzelm <none@none> |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
| #
a1f39138 |
|
07-Oct-2014 |
wenzelm <none@none> |
more antiquotations;
|
| #
2124f5a4 |
|
01-Oct-2014 |
blanchet <none@none> |
documentation
|
| #
67b65fa9 |
|
01-Oct-2014 |
blanchet <none@none> |
fixed a few mistakes in the documentation
|
| #
c5f9b8fb |
|
29-Sep-2014 |
blanchet <none@none> |
reintroduced 'rel_cases' in docs
|
| #
c2456c05 |
|
25-Sep-2014 |
desharna <none@none> |
document 'corec_transfer'
|
| #
7eef29f2 |
|
25-Sep-2014 |
desharna <none@none> |
document 'rec_transfer'
|
| #
35bb7ff5 |
|
19-Sep-2014 |
blanchet <none@none> |
documented limitations
|
| #
8fa9abfe |
|
18-Sep-2014 |
blanchet <none@none> |
fixed attribute name in docs (thanks to Andreas Lochbihler)
|
| #
e19c5ceb |
|
17-Sep-2014 |
blanchet <none@none> |
avoid clash with Quickcheck's generated 'random_xxx' function
|
| #
64feb303 |
|
15-Sep-2014 |
blanchet <none@none> |
set 'mono' attribute on 'rel_mono'
|
| #
7371f09c |
|
15-Sep-2014 |
blanchet <none@none> |
more hints on how to port 'size'
|
| #
6c44e197 |
|
15-Sep-2014 |
blanchet <none@none> |
document size difference
|
| #
6b777fb4 |
|
15-Sep-2014 |
blanchet <none@none> |
generate 'code' attribute only if 'code' plugin is enabled
|
| #
99cb6866 |
|
11-Sep-2014 |
blanchet <none@none> |
tuned documentation
|
| #
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
| #
5209de52 |
|
11-Sep-2014 |
blanchet <none@none> |
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
--HG--
rename : src/HOL/BNF_Examples/Brackin.thy => src/HOL/Datatype_Examples/Brackin.thy
rename : src/HOL/BNF_Examples/Compat.thy => src/HOL/Datatype_Examples/Compat.thy
rename : src/HOL/BNF_Examples/Derivation_Trees/DTree.thy => src/HOL/Datatype_Examples/Derivation_Trees/DTree.thy
rename : src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy => src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy
rename : src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy => src/HOL/Datatype_Examples/Derivation_Trees/Parallel.thy
rename : src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy => src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy
rename : src/HOL/BNF_Examples/Instructions.thy => src/HOL/Datatype_Examples/Instructions.thy
rename : src/HOL/BNF_Examples/IsaFoR_Datatypes.thy => src/HOL/Datatype_Examples/IsaFoR_Datatypes.thy
rename : src/HOL/BNF_Examples/Koenig.thy => src/HOL/Datatype_Examples/Koenig.thy
rename : src/HOL/BNF_Examples/Lambda_Term.thy => src/HOL/Datatype_Examples/Lambda_Term.thy
rename : src/HOL/BNF_Examples/Misc_Codatatype.thy => src/HOL/Datatype_Examples/Misc_Codatatype.thy
rename : src/HOL/BNF_Examples/Misc_Datatype.thy => src/HOL/Datatype_Examples/Misc_Datatype.thy
rename : src/HOL/BNF_Examples/Misc_Primcorec.thy => src/HOL/Datatype_Examples/Misc_Primcorec.thy
rename : src/HOL/BNF_Examples/Misc_Primrec.thy => src/HOL/Datatype_Examples/Misc_Primrec.thy
rename : src/HOL/BNF_Examples/Process.thy => src/HOL/Datatype_Examples/Process.thy
rename : src/HOL/BNF_Examples/SML.thy => src/HOL/Datatype_Examples/SML.thy
rename : src/HOL/BNF_Examples/Stream.thy => src/HOL/Datatype_Examples/Stream.thy
rename : src/HOL/BNF_Examples/Stream_Processor.thy => src/HOL/Datatype_Examples/Stream_Processor.thy
rename : src/HOL/BNF_Examples/TreeFI.thy => src/HOL/Datatype_Examples/TreeFI.thy
rename : src/HOL/BNF_Examples/TreeFsetI.thy => src/HOL/Datatype_Examples/TreeFsetI.thy
rename : src/HOL/BNF_Examples/Verilog.thy => src/HOL/Datatype_Examples/Verilog.thy
|
| #
6a7662be |
|
11-Sep-2014 |
blanchet <none@none> |
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
|
| #
917ff856 |
|
11-Sep-2014 |
blanchet <none@none> |
more docs
|
| #
73c37dfc |
|
09-Sep-2014 |
blanchet <none@none> |
documented extraction plugin
|
| #
c38aae0c |
|
08-Sep-2014 |
blanchet <none@none> |
more docs
|
| #
e9fdc647 |
|
08-Sep-2014 |
blanchet <none@none> |
more documentation
|
| #
da666edb |
|
08-Sep-2014 |
blanchet <none@none> |
compile
|
| #
b8a3e656 |
|
08-Sep-2014 |
blanchet <none@none> |
wildcards in plugins
|
| #
8af04179 |
|
08-Sep-2014 |
blanchet <none@none> |
tuned docs
|
| #
5f759c1d |
|
08-Sep-2014 |
blanchet <none@none> |
updated docs
|
| #
981dcc2f |
|
08-Sep-2014 |
blanchet <none@none> |
more compatibility documentation
|
| #
8bbfc6f8 |
|
04-Sep-2014 |
blanchet <none@none> |
updated docs
|
| #
1c8bb20c |
|
04-Sep-2014 |
blanchet <none@none> |
updated docs
|
| #
1e85c0a7 |
|
02-Sep-2014 |
blanchet <none@none> |
take out 'x = C' of the simplifier for unit types
|
| #
bec91c4f |
|
01-Sep-2014 |
blanchet <none@none> |
compile
|
| #
a50a6cf0 |
|
01-Sep-2014 |
desharna <none@none> |
document 'set_transfer'
|
| #
d52b37b9 |
|
01-Sep-2014 |
desharna <none@none> |
document 'rel_transfer'
|
| #
226bacb3 |
|
01-Sep-2014 |
desharna <none@none> |
document 'map_transfer'
|
| #
43e7a1ac |
|
29-Aug-2014 |
desharna <none@none> |
document 'disc_transfer'
|
| #
d7eef40a |
|
29-Aug-2014 |
desharna <none@none> |
document 'case_transfer'
|
| #
c810fc8c |
|
27-Aug-2014 |
blanchet <none@none> |
removed not so interesting 'set_empty'
|
| #
0b9ca74c |
|
19-Aug-2014 |
desharna <none@none> |
document 'ctr_transfer'
|
| #
38eb3306 |
|
18-Aug-2014 |
blanchet <none@none> |
updated docs
|
| #
89d84638 |
|
18-Aug-2014 |
blanchet <none@none> |
added collection theorem for consistency and convenience
|
| #
6fb4e52a |
|
18-Aug-2014 |
blanchet <none@none> |
reordered some (co)datatype property names for more consistency
|
| #
d52ebfc3 |
|
18-Aug-2014 |
desharna <none@none> |
document 'map_cong_simp'
|
| #
eff16363 |
|
18-Aug-2014 |
desharna <none@none> |
document 'inj_map_strong'
|
| #
68eaaef3 |
|
18-Aug-2014 |
desharna <none@none> |
note 'inj_map' more often
|
| #
c06124ef |
|
14-Aug-2014 |
desharna <none@none> |
document property 'rel_map'
|
| #
3509c85e |
|
11-Aug-2014 |
desharna <none@none> |
document property 'set_cases'
|
| #
2cb65f81 |
|
11-Aug-2014 |
desharna <none@none> |
document property 'set_intros'
|
| #
e6e180c9 |
|
19-Jul-2014 |
blanchet <none@none> |
doc fixes (contributed by Christian Sternagel)
|
| #
519cf191 |
|
16-Jul-2014 |
desharna <none@none> |
document property 'rel_sel'
|
| #
3d51a59e |
|
14-Jul-2014 |
blanchet <none@none> |
took out 'rel_cases' for now because of failing tactic
|
| #
c99bd12b |
|
10-Jul-2014 |
blanchet <none@none> |
more docs
|
| #
4938a6e3 |
|
07-Jul-2014 |
desharna <none@none> |
document property 'rel_cases'
|
| #
9f814f15 |
|
03-Jul-2014 |
desharna <none@none> |
document property 'rel_intros'
|
| #
2fdf6aee |
|
02-Jul-2014 |
desharna <none@none> |
document property 'corec_code'
|
| #
e43563a8 |
|
01-Jul-2014 |
desharna <none@none> |
document property 'rel_induct'
|
| #
3816e708 |
|
27-Jun-2014 |
blanchet <none@none> |
merged two small theory files
|
| #
71005bc5 |
|
30-Jul-2014 |
desharna <none@none> |
document property 'set_induct'
|
| #
f13ba3d9 |
|
24-Jun-2014 |
desharna <none@none> |
document property 'rel_coinduct'
|
| #
42cd340d |
|
10-Jun-2014 |
blanchet <none@none> |
changed syntax of map: and rel: arguments to BNF-based datatypes
|
| #
ed20523b |
|
09-Jun-2014 |
blanchet <none@none> |
use 'where' clause for selector default value syntax
|
| #
6b5a2286 |
|
02-Jun-2014 |
desharna <none@none> |
document property 'sel_set'
|
| #
517cc9da |
|
27-May-2014 |
blanchet <none@none> |
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
|
| #
7e1a5a5b |
|
26-May-2014 |
blanchet <none@none> |
changed '-:' to 'dead' in BNF
|
| #
312f030c |
|
26-May-2014 |
blanchet <none@none> |
got rid of '=:' squiggly
|
| #
11f08ab2 |
|
26-May-2014 |
blanchet <none@none> |
document '=:' syntax better
|
| #
e40c4303 |
|
23-May-2014 |
blanchet <none@none> |
added fifth member to BNF team
|
| #
e83f860e |
|
21-May-2014 |
desharna <none@none> |
document property 'sel_map'
|
| #
4e371cba |
|
19-May-2014 |
blanchet <none@none> |
hide more consts to beautify documentation
|
| #
92b669a2 |
|
19-May-2014 |
desharna <none@none> |
document property 'disc_map_iff'
|
| #
3b8f85e9 |
|
14-May-2014 |
desharna <none@none> |
document 'set_empty'
|
| #
4a681b70 |
|
13-May-2014 |
blanchet <none@none> |
more bnf_decl -> bnf_axiomatization
|
| #
69529447 |
|
13-May-2014 |
blanchet <none@none> |
tuned docs
|
| #
0a4e2a04 |
|
13-May-2014 |
traytel <none@none> |
bnf_decl -> bnf_axiomatization
--HG--
rename : src/HOL/Library/BNF_Decl.thy => src/HOL/Library/BNF_Axiomatization.thy
|
| #
b7c30232 |
|
07-May-2014 |
desharna <none@none> |
document 'map_id0'
|
| #
d9842e68 |
|
08-May-2014 |
desharna <none@none> |
Documented new property
|
| #
66056d47 |
|
23-Apr-2014 |
blanchet <none@none> |
updated BNF docs
|
| #
2216ffbf |
|
23-Apr-2014 |
blanchet <none@none> |
tuned doc comment
|
| #
10afadcb |
|
23-Apr-2014 |
blanchet <none@none> |
updated docs
|
| #
01760a82 |
|
14-Mar-2014 |
blanchet <none@none> |
tuned wording (pun)
|
| #
7e1e76d1 |
|
14-Mar-2014 |
blanchet <none@none> |
document the new 'nonexhaustive' option (cf. 52e8f110fec3)
|
| #
b9ba5739 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'fun_rel' to 'rel_fun'
|
| #
086d90dc |
|
04-Mar-2014 |
blanchet <none@none> |
minor doc fix
|
| #
35d9dd12 |
|
02-Mar-2014 |
blanchet <none@none> |
removed (co)iterators from documentation
|
| #
87d2ff8a |
|
23-Feb-2014 |
blanchet <none@none> |
updated docs
|
| #
2578cf6e |
|
20-Feb-2014 |
blanchet <none@none> |
renamed 'recs' and 'cases' theorems 'rec' and 'case' in old datatype package, for consistency with new package
|
| #
a1d385ea |
|
17-Feb-2014 |
blanchet <none@none> |
renamed 'datatype_new_compat' to 'datatype_compat'
|
| #
44342b4b |
|
17-Feb-2014 |
blanchet <none@none> |
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
|
| #
37e4d09c |
|
13-Feb-2014 |
blanchet <none@none> |
more (co)datatype docs
|
| #
ce6c4368 |
|
13-Feb-2014 |
blanchet <none@none> |
updated docs to reflect the new 'free_constructors' syntax
|
| #
1ae6608b |
|
13-Feb-2014 |
blanchet <none@none> |
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
|
| #
14b3cf57 |
|
13-Feb-2014 |
blanchet <none@none> |
added a bit of documentation for the different commands
|
| #
8cb4a987 |
|
13-Feb-2014 |
blanchet <none@none> |
cleaner, complete proof in documentation, contributed by Dmitriy T.
|
| #
dea2cf15 |
|
12-Feb-2014 |
blanchet <none@none> |
killed 'rep_compat' option
|
| #
2af20090 |
|
12-Feb-2014 |
blanchet <none@none> |
updated docs
|
| #
f49080eb |
|
06-Feb-2014 |
blanchet <none@none> |
more docs
|
| #
3bb95326 |
|
06-Feb-2014 |
blanchet <none@none> |
more docs
|
| #
773a6a0e |
|
06-Feb-2014 |
blanchet <none@none> |
docs
|
| #
6298dbc2 |
|
06-Feb-2014 |
blanchet <none@none> |
docs
|
| #
23cf1679 |
|
06-Feb-2014 |
blanchet <none@none> |
docs about registering a BNF
|
| #
47168367 |
|
03-Feb-2014 |
blanchet <none@none> |
searchable underscores
|
| #
d12a832d |
|
02-Feb-2014 |
blanchet <none@none> |
'primitive' is not an adverb
|
| #
325c96bf |
|
24-Jan-2014 |
blanchet <none@none> |
killed 'More_BNFs' by moving its various bits where they (now) belong
|
| #
9347021a |
|
22-Jan-2014 |
wenzelm <none@none> |
prefer rail cartouche -- avoid back-slashed quotes;
proper documentation of \<newline> syntax;
|
| #
41c735bc |
|
20-Jan-2014 |
blanchet <none@none> |
dissolved BNF session
--HG--
rename : src/HOL/BNF/BNF_Decl.thy => src/HOL/Library/BNF_Decl.thy
rename : src/HOL/Cardinals/Cardinal_Notations.thy => src/HOL/Library/Cardinal_Notations.thy
rename : src/HOL/BNF/Countable_Set_Type.thy => src/HOL/Library/Countable_Set_Type.thy
rename : src/HOL/BNF/More_BNFs.thy => src/HOL/Library/More_BNFs.thy
rename : src/HOL/BNF/Tools/bnf_decl.ML => src/HOL/Library/bnf_decl.ML
|
| #
098b5d30 |
|
20-Jan-2014 |
blanchet <none@none> |
reduced dependencies + updated docs
|
| #
152a3654 |
|
17-Jan-2014 |
wenzelm <none@none> |
clarified @{rail} syntax: prefer explicit \<newline> symbol;
|
| #
033aa506 |
|
09-Jan-2014 |
panny <none@none> |
do not use wrong constructor in auto-generated proof goal
|
| #
c5224a30 |
|
09-Jan-2014 |
blanchet <none@none> |
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
|
| #
45d82a58 |
|
19-Dec-2013 |
blanchet <none@none> |
implemented 'exhaustive' option in tactic
|
| #
d101c24d |
|
02-Dec-2013 |
blanchet <none@none> |
added 'no_code' option
|
| #
0b9d2280 |
|
02-Dec-2013 |
blanchet <none@none> |
revert making 'map_cong' a 'cong' -- it breaks too many proofs in the AFP
|
| #
4071769f |
|
02-Dec-2013 |
blanchet <none@none> |
docs for forgotten BNF theorems
|
| #
066d65e4 |
|
02-Dec-2013 |
blanchet <none@none> |
minor doc update
|
| #
f7ba12b7 |
|
27-Nov-2013 |
traytel <none@none> |
some documentation
|
| #
ae0463c6 |
|
20-Nov-2013 |
blanchet <none@none> |
fixed LaTeX missing }
|
| #
3071c5cb |
|
19-Nov-2013 |
blanchet <none@none> |
updated docs
|
| #
1138e2fb |
|
19-Nov-2013 |
blanchet <none@none> |
case_if -> case_eq_if + docs
|
| #
340b9b02 |
|
12-Nov-2013 |
blanchet <none@none> |
shortened generated property name
|
| #
a6ab8633 |
|
13-Nov-2013 |
traytel <none@none> |
more explicit syntax for defining a bnf
|
| #
7a8e22ca |
|
12-Nov-2013 |
blanchet <none@none> |
document idiomatic use of 'simps_of_case'
|
| #
4a683583 |
|
11-Nov-2013 |
blanchet <none@none> |
minor doc fix
|
| #
da907e8b |
|
06-Nov-2013 |
blanchet <none@none> |
more docs
|
| #
297e99df |
|
06-Nov-2013 |
blanchet <none@none> |
update docs
|
| #
c941fea2 |
|
27-Oct-2013 |
blanchet <none@none> |
commented out vaporware
|
| #
5ab2c60c |
|
22-Oct-2013 |
traytel <none@none> |
update doc according to c0186a0d8cb3
|
| #
8af7759c |
|
21-Oct-2013 |
blanchet <none@none> |
more doc -- feedback from Andrei P.
|
| #
18677507 |
|
21-Oct-2013 |
blanchet <none@none> |
more docs
|
| #
67e54c50 |
|
21-Oct-2013 |
blanchet <none@none> |
more docs
|
| #
40056ab9 |
|
21-Oct-2013 |
blanchet <none@none> |
more docs
|
| #
26bb7144 |
|
21-Oct-2013 |
blanchet <none@none> |
expand doc a bit
|
| #
0bf91ab3 |
|
21-Oct-2013 |
blanchet <none@none> |
updated doc
|
| #
92143a65 |
|
18-Oct-2013 |
blanchet <none@none> |
updated docs
|
| #
6e5fb0cf |
|
18-Oct-2013 |
blanchet <none@none> |
doc fixes suggested by Andreas L.
|
| #
fda568f8 |
|
07-Oct-2013 |
blanchet <none@none> |
more primcorec docs
|
| #
79f1bdbd |
|
07-Oct-2013 |
blanchet <none@none> |
minor doc fix
|
| #
596a95dd |
|
02-Oct-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
5e3796b7 |
|
02-Oct-2013 |
blanchet <none@none> |
minor doc fix (there is no guarantee that the equations for a given f_i are contiguous in the collection)
|
| #
a32752f9 |
|
01-Oct-2013 |
traytel <none@none> |
base the fset bnf on the new FSet theory
|
| #
1345201a |
|
30-Sep-2013 |
blanchet <none@none> |
more "primrec_new" documentation
|
| #
63142116 |
|
26-Sep-2013 |
blanchet <none@none> |
generate "sel_splits(_asm)" theorems
|
| #
0d6756d8 |
|
26-Sep-2013 |
blanchet <none@none> |
generate "sel_exhaust" theorem
|
| #
90ee5d0e |
|
25-Sep-2013 |
blanchet <none@none> |
textual improvements following Christian Sternagel's feedback
|
| #
a22b3ab6 |
|
24-Sep-2013 |
blanchet <none@none> |
renamed generated property
|
| #
f633110c |
|
24-Sep-2013 |
blanchet <none@none> |
updated docs
|
| #
f6105a4c |
|
24-Sep-2013 |
panny <none@none> |
support "of" syntax to disambiguate selector equations
|
| #
e2844b96 |
|
24-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
0677593e |
|
24-Sep-2013 |
blanchet <none@none> |
improved rail diagram
|
| #
5d7ad160 |
|
24-Sep-2013 |
blanchet <none@none> |
use "primcorec" in doc
|
| #
b7cdfcdc |
|
24-Sep-2013 |
panny <none@none> |
add "primcorec" command (cf. ae7f50e70c09)
|
| #
8fd503e1 |
|
23-Sep-2013 |
blanchet <none@none> |
added [code] to selectors
|
| #
93cb4af0 |
|
22-Sep-2013 |
blanchet <none@none> |
set [code] on case equations
|
| #
f84f61b3 |
|
20-Sep-2013 |
blanchet <none@none> |
renamed "primcorec" to "primcorecursive", to open the door to a 'theory -> theory' command called "primcorec" (cf. "fun" vs. "function")
|
| #
2449df45 |
|
20-Sep-2013 |
blanchet <none@none> |
more primcorec docs
|
| #
d13f2af9 |
|
20-Sep-2013 |
blanchet <none@none> |
added primcorec examples with lambdas
|
| #
17f0bd69 |
|
20-Sep-2013 |
blanchet <none@none> |
more primcorec docs
|
| #
98b69a7b |
|
20-Sep-2013 |
blanchet <none@none> |
adapted primcorec documentation to reflect the three views
|
| #
ac85bd71 |
|
19-Sep-2013 |
blanchet <none@none> |
updated docs
|
| #
97a1a87c |
|
18-Sep-2013 |
panny <none@none> |
generate more theorems (e.g. for types with only one constructor)
|
| #
c345bd22 |
|
18-Sep-2013 |
blanchet <none@none> |
updated docs
|
| #
f2c24386 |
|
18-Sep-2013 |
blanchet <none@none> |
use singular to avoid confusion
|
| #
00c920ad |
|
18-Sep-2013 |
blanchet <none@none> |
fixed embarrassing typo in example
|
| #
f4a69813 |
|
16-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
90abf5b5 |
|
16-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
7e48e325 |
|
16-Sep-2013 |
panny <none@none> |
prove simp theorems for newly generated definitions
--HG--
extra : amend_source : 80461d4bf34ca7384a64684b6882b2eeac9ba733
|
| #
a5b509fb |
|
15-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
05868885 |
|
15-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
e5f97dd3 |
|
15-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
f1cd84d2 |
|
15-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
8d77ac83 |
|
15-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
6733b78a |
|
13-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
5fce6449 |
|
13-Sep-2013 |
blanchet <none@none> |
more (co)data doc
|
| #
f1874cf4 |
|
13-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
6ac6a2de |
|
13-Sep-2013 |
blanchet <none@none> |
more (co)data doc
|
| #
f43025c2 |
|
12-Sep-2013 |
blanchet <none@none> |
add a notice to myself in doc
|
| #
4f1c800e |
|
11-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
eaaa53cb |
|
11-Sep-2013 |
blanchet <none@none> |
avoid a keyword
|
| #
d0bf19e0 |
|
11-Sep-2013 |
blanchet <none@none> |
more (co)datatype docs
|
| #
6bca411e |
|
11-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
c9028f96 |
|
11-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
ee30348a |
|
11-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
d2ab42ee |
|
11-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
bf9543e7 |
|
11-Sep-2013 |
blanchet <none@none> |
more (co)datatype documentation
|
| #
685f44f1 |
|
09-Sep-2013 |
blanchet <none@none> |
more docs
|
| #
5168736a |
|
30-Aug-2013 |
panny <none@none> |
fixed bug in primrec_new (allow indirect recursion through constructor arguments other than the first)
|
| #
f3cd6df6 |
|
30-Aug-2013 |
traytel <none@none> |
Doc improvements
|
| #
0bf8afcf |
|
30-Aug-2013 |
traytel <none@none> |
prove theorem in the right context (that knows about local variables)
|
| #
bbec633e |
|
30-Aug-2013 |
blanchet <none@none> |
fixed docs w.r.t. availability of "primrec_new" and friends
|
| #
f8c852c0 |
|
29-Aug-2013 |
blanchet <none@none> |
rationalize message generation + added a warning
|
| #
f620b15a |
|
29-Aug-2013 |
blanchet <none@none> |
documentation ideas
|
| #
a92239d7 |
|
22-Aug-2013 |
blanchet <none@none> |
ideas for (co)datatype docs
|
| #
286d3cf2 |
|
14-Aug-2013 |
blanchet <none@none> |
more (co)datatype documentation
|
| #
e3c4897a |
|
13-Aug-2013 |
blanchet <none@none> |
more work on (co)datatype docs
|
| #
96f89d8a |
|
13-Aug-2013 |
blanchet <none@none> |
added rail diagram
|
| #
ad89385d |
|
12-Aug-2013 |
blanchet <none@none> |
clarified option name (since case/fold/rec are also destructors)
|
| #
b33bf017 |
|
06-Aug-2013 |
blanchet <none@none> |
export ML function (for primcorec)
|
| #
aba62bdd |
|
02-Aug-2013 |
blanchet <none@none> |
more (co)datatype docs
|
| #
251dc7a0 |
|
02-Aug-2013 |
blanchet <none@none> |
more (co)datatype documentation
|
| #
1738e3e4 |
|
02-Aug-2013 |
blanchet <none@none> |
more (co)datatype documentation
|
| #
5c1d4937 |
|
01-Aug-2013 |
blanchet <none@none> |
minor doc fixes
|
| #
33945aa7 |
|
01-Aug-2013 |
blanchet <none@none> |
more (co)datatype docs
|
| #
5196ae80 |
|
01-Aug-2013 |
blanchet <none@none> |
more (co)datatype documentation
|
| #
84a7ed03 |
|
01-Aug-2013 |
blanchet <none@none> |
more (co)datatype documentation
|
| #
3088ce6b |
|
01-Aug-2013 |
blanchet <none@none> |
more (co)datatype docs
|
| #
112dfbce |
|
31-Jul-2013 |
blanchet <none@none> |
more work on (co)datatype docs
|
| #
015fe303 |
|
31-Jul-2013 |
blanchet <none@none> |
more (co)datatype documentation
|
| #
fe878dce |
|
30-Jul-2013 |
blanchet <none@none> |
removed spurious headings
|
| #
aebbc1ba |
|
30-Jul-2013 |
blanchet <none@none> |
more (co)datatype documentation
|
| #
0d770f06 |
|
30-Jul-2013 |
blanchet <none@none> |
sketched documentation for new (co)datatype package
|