#
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
|