| #
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;
|
| #
b00a1738 |
|
27-Mar-2019 |
wenzelm <none@none> |
more informative Spec_Rules.Equational: support corecursion;
|
| #
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;
|
| #
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)'
|
| #
659a2dbd |
|
20-Dec-2016 |
blanchet <none@none> |
generalized ML function (towards nonuniform datatypes)
|
| #
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
|
| #
280971b2 |
|
30-Aug-2016 |
traytel <none@none> |
generate proper goal when equation is entered programmatically
|
| #
41f01a69 |
|
23-Aug-2016 |
traytel <none@none> |
tuned signature
|
| #
bee57ad5 |
|
23-Jun-2016 |
wenzelm <none@none> |
tuned signature;
|
| #
46bb214d |
|
11-Jun-2016 |
wenzelm <none@none> |
clarified syntax;
|
| #
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);
|
| #
86d79029 |
|
30-May-2016 |
wenzelm <none@none> |
allow 'for' fixes for multi_specs;
|
| #
68f9ecca |
|
28-Apr-2016 |
wenzelm <none@none> |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;
|
| #
fe42a4e9 |
|
22-Mar-2016 |
blanchet <none@none> |
tuned whitespace
|
| #
7674b664 |
|
22-Mar-2016 |
blanchet <none@none> |
export ML function
|
| #
35afd302 |
|
10-Mar-2016 |
blanchet <none@none> |
don't throw an exception when trying to print an error message
|
| #
a2073db7 |
|
10-Mar-2016 |
blanchet <none@none> |
eta-expansion done right in "primcorec"
|
| #
d5c534a3 |
|
02-Mar-2016 |
traytel <none@none> |
respect qualification when noting theorems in prim(co)rec
|
| #
03d6340d |
|
14-Feb-2016 |
blanchet <none@none> |
clearer error message
|
| #
369e4785 |
|
13-Dec-2015 |
wenzelm <none@none> |
more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;
|
| #
591a7bfe |
|
01-Dec-2015 |
blanchet <none@none> |
tuned whitespace
|
| #
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
| #
b22e4c0f |
|
07-Oct-2015 |
blanchet <none@none> |
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
|
| #
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
|
| #
2813b7ac |
|
25-Sep-2015 |
traytel <none@none> |
more canonical context threading
|
| #
4930226f |
|
06-Sep-2015 |
haftmann <none@none> |
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
|
| #
66dfd9b7 |
|
16-Jul-2015 |
blanchet <none@none> |
made code less loopy
|
| #
bc205fbf |
|
16-Jul-2015 |
blanchet <none@none> |
generalized generic translation function
|
| #
b1e5e464 |
|
13-Jul-2015 |
blanchet <none@none> |
tuning
|
| #
2c9e2e3e |
|
09-Jul-2015 |
blanchet <none@none> |
tuned ML signature (and rationalized code a bit)
|
| #
824aee18 |
|
07-Jul-2015 |
blanchet <none@none> |
tuned ML signature
|
| #
f9ccd3fb |
|
02-Jun-2015 |
wenzelm <none@none> |
clarified context;
|
| #
3f438084 |
|
10-Apr-2015 |
blanchet <none@none> |
renamed ML funs
|
| #
5ae28e01 |
|
10-Apr-2015 |
blanchet <none@none> |
generalized code
|
| #
1009b8d0 |
|
09-Apr-2015 |
blanchet <none@none> |
tuned signature
|
| #
f64d293f |
|
07-Apr-2015 |
blanchet <none@none> |
generalized slightly
|
| #
0b44f209 |
|
07-Apr-2015 |
blanchet <none@none> |
generalized code
|
| #
a0b0cae3 |
|
07-Apr-2015 |
blanchet <none@none> |
generalized code
|
| #
017512d0 |
|
07-Apr-2015 |
blanchet <none@none> |
export ML function
|
| #
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
| #
0e2b1250 |
|
01-Apr-2015 |
blanchet <none@none> |
simplified code
|
| #
03b64291 |
|
30-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
28c21755 |
|
24-Mar-2015 |
wenzelm <none@none> |
clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context;
|
| #
9113f38b |
|
24-Mar-2015 |
blanchet <none@none> |
tuning
|
| #
7f0e77af |
|
10-Mar-2015 |
blanchet <none@none> |
export more functions (for future 'corec')
|
| #
2eeb52fe |
|
10-Mar-2015 |
blanchet <none@none> |
tuning
|
| #
73047e78 |
|
10-Mar-2015 |
blanchet <none@none> |
tuning
|
| #
af08be71 |
|
05-Mar-2015 |
blanchet <none@none> |
avoid needless 'if ... undefined' in generated theorems
|
| #
73c5a6d6 |
|
05-Mar-2015 |
blanchet <none@none> |
deal better with corecursion through functions
|
| #
09d35824 |
|
05-Mar-2015 |
blanchet <none@none> |
removed too strict checks
|
| #
5d8b316c |
|
04-Mar-2015 |
blanchet <none@none> |
message tuning
|
| #
b6a768f0 |
|
04-Mar-2015 |
blanchet <none@none> |
tuning
|
| #
52019a2c |
|
05-Mar-2015 |
blanchet <none@none> |
improved primcorec messages
|
| #
a9e6ce23 |
|
05-Mar-2015 |
blanchet <none@none> |
improved primcorec messages
|
| #
a8812995 |
|
05-Mar-2015 |
blanchet <none@none> |
better primcorec messages
|
| #
085d0905 |
|
05-Mar-2015 |
blanchet <none@none> |
more primcorec messages
|
| #
44dea20f |
|
05-Mar-2015 |
blanchet <none@none> |
more precise primcorec messages
|
| #
ded52b22 |
|
05-Mar-2015 |
blanchet <none@none> |
more precise primcorec messages
|
| #
9c6a05fb |
|
05-Mar-2015 |
blanchet <none@none> |
better primcorec messages
|
| #
ea3f84a1 |
|
05-Mar-2015 |
blanchet <none@none> |
more 'primcorec' error handling
|
| #
94df6324 |
|
05-Mar-2015 |
blanchet <none@none> |
helpful error message when 'auto' fails
|
| #
7285eaed |
|
05-Mar-2015 |
blanchet <none@none> |
no quick_and_dirty for goals that may fail + tuned messages
|
| #
8b456ccd |
|
05-Mar-2015 |
blanchet <none@none> |
tuned new primrec messages
|
| #
cd55212e |
|
05-Mar-2015 |
blanchet <none@none> |
reworked primcorec error messages
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
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
|
| #
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};
|
| #
83205ee1 |
|
23-Nov-2014 |
blanchet <none@none> |
tuned whitespace
|
| #
c9829f79 |
|
23-Nov-2014 |
blanchet <none@none> |
keep all 'ctr' theorems
|
| #
7aef1c44 |
|
23-Nov-2014 |
blanchet <none@none> |
smoothly handle unit codatatypes in 'primcorec'
|
| #
c3de4772 |
|
23-Nov-2014 |
blanchet <none@none> |
careful with de Bruijn indices
|
| #
cbfdc100 |
|
08-Oct-2014 |
wenzelm <none@none> |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
| #
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
|
| #
05509858 |
|
19-Sep-2014 |
blanchet <none@none> |
more honest 'primcorec' -- don't parse a theorem name that is then ignored
|
| #
28cf91d1 |
|
19-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
78b45325 |
|
19-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
6b777fb4 |
|
15-Sep-2014 |
blanchet <none@none> |
generate 'code' attribute only if 'code' plugin is enabled
|
| #
f08fc76d |
|
09-Sep-2014 |
blanchet <none@none> |
compile
|
| #
02b2c624 |
|
09-Sep-2014 |
blanchet <none@none> |
preserve case names in '(co)induct' theorems generated by prim(co)rec'
|
| #
97822f3a |
|
08-Sep-2014 |
blanchet <none@none> |
export useful functions for users of (co)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
|
| #
d36b3fcf |
|
04-Sep-2014 |
blanchet <none@none> |
fixed infinite loops in 'register' functions + more uniform API
|
| #
a5355909 |
|
01-Sep-2014 |
blanchet <none@none> |
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
|
| #
12b0bc3d |
|
01-Sep-2014 |
blanchet <none@none> |
compile
|
| #
9c861e3b |
|
01-Sep-2014 |
blanchet <none@none> |
more compatibility between old- and new-style datatypes
|
| #
6fb4e52a |
|
18-Aug-2014 |
blanchet <none@none> |
reordered some (co)datatype property names for more consistency
|
| #
4bbbfbf8 |
|
12-Aug-2014 |
blanchet <none@none> |
less aggressive unfolding; removed debugging;
|
| #
877dea0b |
|
13-Jul-2014 |
panny <none@none> |
fix typo
|
| #
ff38f8ec |
|
13-Jul-2014 |
panny <none@none> |
throw error for bad input
|
| #
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
|
| #
020ff44f |
|
24-Jun-2014 |
desharna <none@none> |
tune the implementation of 'rel_coinduct'
|
| #
9bcd2c04 |
|
13-May-2014 |
blanchet <none@none> |
tuning
|
| #
bfd5d2c4 |
|
05-May-2014 |
blanchet <none@none> |
simplify selectors in code views
|
| #
6fed8b0b |
|
01-May-2014 |
panny <none@none> |
use qualified name (was interpreted as a catch-all variable name)
|
| #
3b9d5410 |
|
01-May-2014 |
panny <none@none> |
add additional check to avoid selector formula right-hand side consisting of a nullary constructor getting interpreted as a discriminator formula
|
| #
3c4f4261 |
|
22-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
| #
b1c07ea3 |
|
14-Mar-2014 |
panny <none@none> |
add error messages for invalid inputs
|
| #
c4dc0538 |
|
07-Mar-2014 |
blanchet <none@none> |
use balanced tuples in 'primcorec'
|
| #
d815b696 |
|
06-Mar-2014 |
blanchet <none@none> |
balance tuples that represent curried functions
|
| #
35d9dd12 |
|
02-Mar-2014 |
blanchet <none@none> |
removed (co)iterators from documentation
|
| #
e3abe18d |
|
02-Mar-2014 |
blanchet <none@none> |
avoid duplicate 'disc_iff' theorems
|
| #
c39b02f9 |
|
02-Mar-2014 |
blanchet <none@none> |
rationalized internals
|
| #
b29ffe0e |
|
02-Mar-2014 |
blanchet <none@none> |
rationalize internals
|
| #
8bc18da0 |
|
02-Mar-2014 |
blanchet <none@none> |
make 'diff_iff' a simp rule if available
|
| #
60d22fd5 |
|
02-Mar-2014 |
blanchet <none@none> |
less aggressive resolving
|
| #
ae64540a |
|
27-Feb-2014 |
blanchet <none@none> |
correct most general type for mutual recursion when several identical types are involved
|
| #
efebaf05 |
|
18-Feb-2014 |
blanchet <none@none> |
prepare two-stage 'primrec' setup
|
| #
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'
|
| #
0837409d |
|
17-Feb-2014 |
blanchet <none@none> |
tuning: moved code where it belongs
|
| #
79b9f515 |
|
17-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
0ba161cf |
|
14-Feb-2014 |
blanchet <none@none> |
allow different functions to recurse on the same type, like in the old package
|
| #
60177433 |
|
13-Feb-2014 |
blanchet <none@none> |
added 'Spec_Rules' for 'primcorec'
|
| #
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
| #
4b092e5d |
|
12-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
4bb4d1f9 |
|
05-Feb-2014 |
blanchet <none@none> |
don't waste time with old-style 'case's that don't have the required theorems
|
| #
4fd2a4ce |
|
05-Feb-2014 |
blanchet <none@none> |
expand 'split' in direct corecursion as well
|
| #
c0de7553 |
|
05-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
fd5d98a4 |
|
05-Feb-2014 |
blanchet <none@none> |
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
|
| #
e47f2f4b |
|
05-Feb-2014 |
blanchet <none@none> |
properly massage 'if's / 'case's etc. under lambdas
|
| #
b92f9a76 |
|
21-Jan-2014 |
blanchet <none@none> |
made SML/NJ happier
|
| #
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
|