equal
deleted
inserted
replaced
33 |
33 |
34 |
34 |
35 Minor fixes in the tutorial |
35 Minor fixes in the tutorial |
36 =========================== |
36 =========================== |
37 |
37 |
|
38 Adjust FP textbook refs: new Bird, Hudak |
|
39 Discrete math textbook: Rosen? |
|
40 |
|
41 say something about "abbreviations" when defs are introduced. |
|
42 |
38 adjust type of ^ in tab:overloading |
43 adjust type of ^ in tab:overloading |
39 |
|
40 explanation of term "contrapositive"/contraposition in Rules? |
|
41 Index the notion and maybe the rules contrapos_xy |
|
42 |
|
43 get rid of use_thy in tutorial? |
|
44 |
|
45 Orderings on numbers (with hint that it is overloaded): |
|
46 bounded quantifers ALL x<y, <=. |
|
47 |
44 |
48 an example of induction: !y. A --> B --> C ?? |
45 an example of induction: !y. A --> B --> C ?? |
49 |
46 |
50 Explain type_definition and mention pre-proved thms in subset.thy? |
47 Explain type_definition and mention pre-proved thms in subset.thy? |
51 -> Types/typedef |
48 -> Types/typedef |
71 |
68 |
72 Minor additions to the tutorial, unclear where |
69 Minor additions to the tutorial, unclear where |
73 ============================================== |
70 ============================================== |
74 |
71 |
75 unfold? |
72 unfold? |
76 |
|
77 Tacticals: , ? + |
|
78 Note: + is used in typedef section! |
|
79 |
|
80 A list of further useful commands (rules? tricks?) |
|
81 prefer, defer, print_simpset (-> print_simps?) |
|
82 |
|
83 demonstrate x : set xs in Sets. Or Tricks chapter? |
|
84 |
|
85 Appendix with HOL and Isar keywords. |
|
86 |
73 |
87 |
74 |
88 Possible exercises |
75 Possible exercises |
89 ================== |
76 ================== |
90 |
77 |