equal
deleted
inserted
replaced
38 adjust type of ^ in tab:overloading |
38 adjust type of ^ in tab:overloading |
39 |
39 |
40 explanation of term "contrapositive"/contraposition in Rules? |
40 explanation of term "contrapositive"/contraposition in Rules? |
41 Index the notion and maybe the rules contrapos_xy |
41 Index the notion and maybe the rules contrapos_xy |
42 |
42 |
43 If Advanced and Types chapter ar swapped: |
|
44 Make forward ref from ... = True in Axioms to preprocessor section. |
|
45 |
|
46 get rid of use_thy in tutorial? |
43 get rid of use_thy in tutorial? |
47 |
44 |
48 Orderings on numbers (with hint that it is overloaded): |
45 Orderings on numbers (with hint that it is overloaded): |
49 bounded quantifers ALL x<y, <=. |
46 bounded quantifers ALL x<y, <=. |
50 |
47 |
73 |
70 |
74 |
71 |
75 Minor additions to the tutorial, unclear where |
72 Minor additions to the tutorial, unclear where |
76 ============================================== |
73 ============================================== |
77 |
74 |
78 case_tac on bool? |
75 unfold? |
79 |
76 |
80 Tacticals: , ? + |
77 Tacticals: , ? + |
81 Note: + is used in typedef section! |
78 Note: + is used in typedef section! |
82 |
79 |
83 A list of further useful commands (rules? tricks?) |
80 A list of further useful commands (rules? tricks?) |
84 prefer, defer, print_simpset (-> print_simps?) |
81 prefer, defer, print_simpset (-> print_simps?) |
85 |
|
86 Advanced Ind expects rule_format incl (no_asm) (which it currently explains!) |
|
87 Where explained? Should go into a separate section as Inductive needs it as |
|
88 well. |
|
89 |
82 |
90 demonstrate x : set xs in Sets. Or Tricks chapter? |
83 demonstrate x : set xs in Sets. Or Tricks chapter? |
91 |
84 |
92 Appendix with HOL and Isar keywords. |
85 Appendix with HOL and Isar keywords. |
93 |
86 |