| #
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;
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
ea4853ba |
|
28-Jan-2018 |
wenzelm <none@none> |
clarified take/drop/chop prefix/suffix;
|
| #
548cd1f9 |
|
20-Jul-2017 |
blanchet <none@none> |
strengthened tactic
|
| #
77a9e73c |
|
19-Jul-2017 |
blanchet <none@none> |
strengthened tactic (for 'fun' BNF)
|
| #
9322bd71 |
|
02-Jul-2017 |
haftmann <none@none> |
proper concept of code declaration wrt. atomicity and Isar declarations
--HG--
extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472
|
| #
502ab55a |
|
30-Dec-2016 |
blanchet <none@none> |
more uniform errors in '(prim)(co)rec(ursive)' variants
|
| #
bb1d3a61 |
|
28-Dec-2016 |
blanchet <none@none> |
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
|
| #
41f01a69 |
|
23-Aug-2016 |
traytel <none@none> |
tuned signature
|
| #
2e392e73 |
|
06-Jun-2016 |
haftmann <none@none> |
explicit tagging of code equations de-baroquifies interface
--HG--
extra : rebase_source : 1d83d31f669dc30b586df508a64fdc3a9e7b2655
|
| #
cd5814d0 |
|
30-May-2016 |
wenzelm <none@none> |
tuned;
|
| #
68f9ecca |
|
28-Apr-2016 |
wenzelm <none@none> |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;
|
| #
d5c534a3 |
|
02-Mar-2016 |
traytel <none@none> |
respect qualification when noting theorems in prim(co)rec
|
| #
d39b0ef7 |
|
17-Feb-2016 |
blanchet <none@none> |
allow predicator instead of map function in 'primrec'
|
| #
6c503036 |
|
16-Feb-2016 |
blanchet <none@none> |
avoid duplicate theorems in 'primrec's result when invoked programmatically
|
| #
591a7bfe |
|
01-Dec-2015 |
blanchet <none@none> |
tuned whitespace
|
| #
2813b7ac |
|
25-Sep-2015 |
traytel <none@none> |
more canonical context threading
|
| #
dbbe37ca |
|
15-Jul-2015 |
traytel <none@none> |
{r,e,d,f}tac with proper context in BNF
|
| #
3fd8bf9b |
|
10-Apr-2015 |
wenzelm <none@none> |
make SML/NJ more happy;
|
| #
02fcb3d9 |
|
10-Apr-2015 |
blanchet <none@none> |
have 'primrec' return definitions
|
| #
3f438084 |
|
10-Apr-2015 |
blanchet <none@none> |
renamed ML funs
|
| #
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
| #
03b64291 |
|
30-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
2eeb52fe |
|
10-Mar-2015 |
blanchet <none@none> |
tuning
|
| #
8b456ccd |
|
05-Mar-2015 |
blanchet <none@none> |
tuned new primrec messages
|
| #
e3153e9f |
|
11-Jan-2015 |
wenzelm <none@none> |
tuned warnings: observe Context_Position.is_visible;
|
| #
d9c8335a |
|
05-Jan-2015 |
blanchet <none@none> |
generate [code] only with 'code' plugin enabled
|
| #
1de6462a |
|
05-Jan-2015 |
blanchet <none@none> |
added plugins syntax to prim(co)rec
|
| #
ccc25809 |
|
05-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};
|
| #
56b8a931 |
|
13-Nov-2014 |
traytel <none@none> |
do not introduce consts too early unnecessarily
|
| #
cbfdc100 |
|
08-Oct-2014 |
wenzelm <none@none> |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
| #
b0d7f95d |
|
19-Sep-2014 |
blanchet <none@none> |
made new 'primrec' bootstrapping-capable
|
| #
232ad5b3 |
|
19-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
78b45325 |
|
19-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
4264224c |
|
11-Sep-2014 |
blanchet <none@none> |
tuning terminology
|
| #
23a5af3d |
|
11-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
ffcb201a |
|
11-Sep-2014 |
blanchet <none@none> |
fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
|
| #
e6e1fcc4 |
|
11-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
ed623a2e |
|
11-Sep-2014 |
blanchet <none@none> |
fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'
|
| #
02b2c624 |
|
09-Sep-2014 |
blanchet <none@none> |
preserve case names in '(co)induct' theorems generated by prim(co)rec'
|
| #
3d4ab033 |
|
09-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
97822f3a |
|
08-Sep-2014 |
blanchet <none@none> |
export useful functions for users of (co)recursors
|
| #
b8a3e656 |
|
08-Sep-2014 |
blanchet <none@none> |
wildcards in plugins
|
| #
75fd5395 |
|
08-Sep-2014 |
blanchet <none@none> |
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
|
| #
d36b3fcf |
|
04-Sep-2014 |
blanchet <none@none> |
fixed infinite loops in 'register' functions + more uniform API
|
| #
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
|
| #
8c308eea |
|
23-Jul-2014 |
blanchet <none@none> |
repaired named derivations
|
| #
5fc12b85 |
|
13-Jul-2014 |
panny <none@none> |
catch "not found" case
|
| #
52e1ed24 |
|
07-Jul-2014 |
desharna <none@none> |
add helper function map_prod
|
| #
c1bd04e5 |
|
27-Jun-2014 |
blanchet <none@none> |
compile
|
| #
6f5ea271 |
|
27-Jun-2014 |
blanchet <none@none> |
tuned variable names
|
| #
9bcd2c04 |
|
13-May-2014 |
blanchet <none@none> |
tuning
|
| #
df61e430 |
|
05-May-2014 |
blanchet <none@none> |
note correct induction schemes in 'primrec' (for N2M)
|
| #
aea2cf85 |
|
23-Apr-2014 |
blanchet <none@none> |
localize new size function generation code
|
| #
df15a7e7 |
|
23-Apr-2014 |
blanchet <none@none> |
generate size instances for new-style datatypes
|
| #
3c4f4261 |
|
22-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
| #
6ec65b50 |
|
13-Mar-2014 |
panny <none@none> |
print warning if some constructors are missing;
make this warning optional via "(nonexhaustive)"
--HG--
extra : amend_source : e45d28e2e522a655f97c82485467aefdb4ab6213
|
| #
c39b02f9 |
|
02-Mar-2014 |
blanchet <none@none> |
rationalized internals
|
| #
ae64540a |
|
27-Feb-2014 |
blanchet <none@none> |
correct most general type for mutual recursion when several identical types are involved
|
| #
88a9bdca |
|
19-Feb-2014 |
blanchet <none@none> |
adapted Nitpick to 'primrec' refactoring
|
| #
04523a1c |
|
19-Feb-2014 |
blanchet <none@none> |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
| #
d9694910 |
|
19-Feb-2014 |
blanchet <none@none> |
rewrote a small portion of code to avoid dependency on low-level constant
|
| #
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
|
| #
a4bafeb9 |
|
17-Feb-2014 |
blanchet <none@none> |
tuning
* * *
moved 'primrec' up to displace the few remaining uses of 'old_primrec'
|
| #
99807201 |
|
17-Feb-2014 |
blanchet <none@none> |
name derivations in 'primrec' for code extraction from proof terms
|
| #
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)
|
| #
0837409d |
|
17-Feb-2014 |
blanchet <none@none> |
tuning: moved code where it belongs
|
| #
6f97f4d1 |
|
17-Feb-2014 |
blanchet <none@none> |
have 'primrec_new' fall back on old 'primrec' when given old-style datatypes
|
| #
79b9f515 |
|
17-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
25f53062 |
|
14-Feb-2014 |
blanchet <none@none> |
removed assumption in 'primrec_new' that a given constructor can only occur once
|
| #
0ba161cf |
|
14-Feb-2014 |
blanchet <none@none> |
allow different functions to recurse on the same type, like in the old package
|
| #
f1150872 |
|
13-Feb-2014 |
blanchet <none@none> |
have 'Ctr_Sugar' register its 'Spec_Rules'
|
| #
88a2727e |
|
20-Jan-2014 |
blanchet <none@none> |
tuned names
|
| #
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
|