| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
8aafd76b |
|
26-Oct-2016 |
blanchet <none@none> |
tuning
|
| #
bd27a761 |
|
12-Sep-2016 |
blanchet <none@none> |
prove 'set' property backward
|
| #
79f97a31 |
|
08-Sep-2016 |
blanchet <none@none> |
tuning
|
| #
25f52df5 |
|
06-Sep-2016 |
blanchet <none@none> |
tuned ML signature
|
| #
0e3f246a |
|
05-Sep-2016 |
blanchet <none@none> |
exported ML functions
|
| #
5339f05b |
|
05-Jul-2016 |
wenzelm <none@none> |
more antiquotations;
|
| #
237f0cff |
|
02-Jun-2016 |
wenzelm <none@none> |
eliminated pointless alias (no warning for duplicates);
|
| #
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
| #
6b18406f |
|
16-Feb-2016 |
traytel <none@none> |
make predicator a first-class bnf citizen
|
| #
2678006a |
|
11-Jan-2016 |
blanchet <none@none> |
exported ML function
|
| #
44916bcd |
|
24-Sep-2015 |
wenzelm <none@none> |
explicit indication of overloaded typedefs;
|
| #
3349054e |
|
23-Sep-2015 |
traytel <none@none> |
more useful properties of the relators
|
| #
f2fecee2 |
|
03-Sep-2015 |
wenzelm <none@none> |
more general Typedef.bindings;
tuned signature;
|
| #
78d8b09f |
|
03-Sep-2015 |
traytel <none@none> |
use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
|
| #
093cea8d |
|
31-Mar-2015 |
wenzelm <none@none> |
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
|
| #
03b64291 |
|
30-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
5b8baa9f |
|
30-Mar-2015 |
wenzelm <none@none> |
support for strictly private name space entries;
tuned signature;
|
| #
1426640f |
|
30-Mar-2015 |
blanchet <none@none> |
export more low-level theorems in data structure (partly for 'corec')
|
| #
7f6d59a0 |
|
19-Dec-2014 |
desharna <none@none> |
generate 'disc_eq_case' for Ctr_Sugars
|
| #
4f36e217 |
|
11-Dec-2014 |
traytel <none@none> |
conceal typedef more violently
|
| #
9e653fc8 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper proof context for typedef;
|
| #
b1da3206 |
|
30-Oct-2014 |
wenzelm <none@none> |
proper syntax categery "name" -- as usual and as documented;
|
| #
f05f85f5 |
|
14-Oct-2014 |
desharna <none@none> |
generate 'sel_transfer' for (co)datatypes
|
| #
ce27dd00 |
|
13-Oct-2014 |
wenzelm <none@none> |
tuned signature;
|
| #
cbfdc100 |
|
08-Oct-2014 |
wenzelm <none@none> |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
| #
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'
|
| #
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'
|
| #
e05be41f |
|
25-Sep-2014 |
desharna <none@none> |
generate 'rec_transfer' for datatypes
|
| #
0ecf02ae |
|
08-Sep-2014 |
blanchet <none@none> |
removed comment (yes, this is different -- add_typedef_global will fail in a locale with assumptions)
|
| #
e8d97a27 |
|
08-Sep-2014 |
blanchet <none@none> |
added flag to 'typedef' to allow concealed definitions
|
| #
241c5b8f |
|
08-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
ec4e6125 |
|
04-Sep-2014 |
blanchet <none@none> |
tuned size function generation
|
| #
8ba9107a |
|
07-Jul-2014 |
desharna <none@none> |
refactor some tactics
|
| #
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
|
| #
7e1a5a5b |
|
26-May-2014 |
blanchet <none@none> |
changed '-:' to 'dead' in BNF
|
| #
312f030c |
|
26-May-2014 |
blanchet <none@none> |
got rid of '=:' squiggly
|
| #
1c1981c6 |
|
27-Apr-2014 |
blanchet <none@none> |
cleaner 'rel_inject' theorems
|
| #
173cad60 |
|
23-Apr-2014 |
blanchet <none@none> |
manual merge + added 'rel_distincts' field to record for symmetry
|
| #
72596a3c |
|
23-Apr-2014 |
blanchet <none@none> |
generate 'rec_o_map' and 'size_o_map' in size extension
|
| #
939a8149 |
|
23-Apr-2014 |
blanchet <none@none> |
added 'inj_map' as auxiliary BNF theorem
|
| #
8d0ad389 |
|
10-Apr-2014 |
kuncar <none@none> |
export theorems
|
| #
12157cd1 |
|
19-Mar-2014 |
haftmann <none@none> |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
| #
b9ba5739 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'fun_rel' to 'rel_fun'
|
| #
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
|
| #
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
|
| #
8e6ecc59 |
|
13-Feb-2014 |
blanchet <none@none> |
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
|
| #
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
|