48 |
48 |
49 Explain typographic conventions? |
49 Explain typographic conventions? |
50 |
50 |
51 an example of induction: !y. A --> B --> C ?? |
51 an example of induction: !y. A --> B --> C ?? |
52 |
52 |
53 Advanced Ind expects rule_format incl (no_asm) (which it currently explains! |
|
54 Where explained? |
|
55 |
|
56 Appendix: Lexical: long ids. |
53 Appendix: Lexical: long ids. |
57 |
54 |
58 Warning: infixes automatically become reserved words! |
55 Warning: infixes automatically become reserved words! |
59 |
56 |
60 Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof? |
57 Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof? |
81 print_simpset (-> print_simps?) |
78 print_simpset (-> print_simps?) |
82 (Another subsection Useful theorems, methods, and commands?) |
79 (Another subsection Useful theorems, methods, and commands?) |
83 |
80 |
84 Mention that simp etc (big step tactics) insist on change? |
81 Mention that simp etc (big step tactics) insist on change? |
85 |
82 |
86 Explain what "by" and "." really do, and introduce "done". |
83 Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it |
|
84 does more.) |
87 |
85 |
88 A list of further useful commands (rules? tricks?) |
86 A list of further useful commands (rules? tricks?) |
89 prefer, defer |
87 prefer, defer |
90 |
88 |
91 An overview of the automatic methods: simp, auto, fast, blast, force, |
89 An overview of the automatic methods: simp, auto, fast, blast, force, |
92 clarify, clarsimp (intro, elim?) |
90 clarify, clarsimp (intro, elim?) |
93 |
91 |
94 explain rulify before induction section? |
92 Advanced Ind expects rule_format incl (no_asm) (which it currently explains!) |
|
93 Where explained? |
|
94 Inductive also needs rule_format! |
|
95 |
|
96 Where is "simplified" explained? Needed by Inductive/AB.thy |
95 |
97 |
96 demonstrate x : set xs in Sets. Or Tricks chapter? |
98 demonstrate x : set xs in Sets. Or Tricks chapter? |
97 |
99 |
98 Appendix with HOL keywords. Say something about other keywords. |
100 Appendix with HOL keywords. Say something about other keywords. |
99 |
101 |