equal
deleted
inserted
replaced
1 Implementation |
1 Implementation |
2 ============== |
2 ============== |
3 |
3 |
4 Why is comp needed in addition to op O? |
4 Relation: comp -> composition |
5 Explain in syntax section! |
|
6 |
5 |
7 replace "simp only split" by "split_tac". |
6 replace "simp only split" by "split_tac". |
8 |
|
9 arithmetic: allow mixed nat/int formulae |
|
10 -> simplify proof of part1 in Inductive/AB.thy |
|
11 |
7 |
12 Add map_cong?? (upto 10% slower) |
8 Add map_cong?? (upto 10% slower) |
13 |
9 |
14 Recdef: Get rid of function name in header. |
10 Recdef: Get rid of function name in header. |
15 Support mutual recursion (Konrad?) |
11 Support mutual recursion (Konrad?) |
28 More predefined functions for datatypes: map? |
24 More predefined functions for datatypes: map? |
29 |
25 |
30 Induction rules for int: int_le/ge_induct? |
26 Induction rules for int: int_le/ge_induct? |
31 Needed for ifak example. But is that example worth it? |
27 Needed for ifak example. But is that example worth it? |
32 |
28 |
|
29 Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was |
|
30 ein generelles Feature ist, das man vielleicht mal abstellen sollte. |
|
31 |
33 proper mutual simplification |
32 proper mutual simplification |
34 |
33 |
35 defs with = and pattern matching?? |
34 defs with = and pattern matching?? |
36 |
35 |
37 |
36 |
59 Appendix: Lexical: long ids. |
58 Appendix: Lexical: long ids. |
60 |
59 |
61 Warning: infixes automatically become reserved words! |
60 Warning: infixes automatically become reserved words! |
62 |
61 |
63 Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof? |
62 Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof? |
64 |
|
65 mention split_split in advanced pair section. |
|
66 |
63 |
67 recdef with nested recursion: either an example or at least a pointer to the |
64 recdef with nested recursion: either an example or at least a pointer to the |
68 literature. In Recdef/termination.thy, at the end. |
65 literature. In Recdef/termination.thy, at the end. |
69 %FIXME, with one exception: nested recursion. |
66 %FIXME, with one exception: nested recursion. |
70 |
67 |