34 apply(substitute [2] thm) |
34 apply(substitute [2] thm) |
35 |
35 |
36 it would be nice if @term could deal with ?-vars. |
36 it would be nice if @term could deal with ?-vars. |
37 then a number of (unchecked!) @texts could be converted to @terms. |
37 then a number of (unchecked!) @texts could be converted to @terms. |
38 |
38 |
|
39 it would be nice if one could get id to the enclosing quotes in the [source] option. |
|
40 |
39 |
41 |
40 Minor fixes in the tutorial |
42 Minor fixes in the tutorial |
41 =========================== |
43 =========================== |
42 |
44 |
43 replace simp only split by split_tac. |
45 replace simp only split by split_tac. |
47 Explain typographic conventions? |
49 Explain typographic conventions? |
48 |
50 |
49 an example of induction: !y. A --> B --> C ?? |
51 an example of induction: !y. A --> B --> C ?? |
50 |
52 |
51 Advanced Ind expects rulify, mp and spec. How much really? |
53 Advanced Ind expects rulify, mp and spec. How much really? |
52 |
|
53 recdef: subsection Beyond Measure on lex, finite_psubset, ... |
|
54 incl Ackermann, which is now at the end of Recdef/termination.thy. |
|
55 -> Advanced. |
|
56 Sentence at the end: |
|
57 If you feel that the definition of recursive functions is overly and maybe |
|
58 unnecessarily complicated by the requirement of totality you should ponder |
|
59 the alternative, a logic of partial functions, where recursive definitions |
|
60 are always wellformed. For a start, there are many |
|
61 such logics, and no clear winner has emerged. And in all of these logics you |
|
62 are (more or less frequently) required to reason about the definedness of |
|
63 terms explicitly. Thus one shifts definedness arguments from definition to |
|
64 proof time. In HOL you may have to work hard to define a function, but proofs |
|
65 can then proceed unencumbered by worries about undefinedness. |
|
66 |
54 |
67 Appendix: Lexical: long ids. |
55 Appendix: Lexical: long ids. |
68 |
56 |
69 Warning: infixes automatically become reserved words! |
57 Warning: infixes automatically become reserved words! |
70 |
58 |