equal
deleted
inserted
replaced
59 |
59 |
60 I guess we should say "HOL" everywhere, with a remark early on about the |
60 I guess we should say "HOL" everywhere, with a remark early on about the |
61 differences between our HOL and the other one. |
61 differences between our HOL and the other one. |
62 |
62 |
63 Syntax translations! Harpoons already used! |
63 Syntax translations! Harpoons already used! |
|
64 say something about "abbreviations" when defs are introduced. |
64 |
65 |
65 warning: simp of asms from l to r; may require reordering (rotate_tac) |
66 warning: simp of asms from l to r; may require reordering (rotate_tac) |
66 |
67 |
67 Adjust FP textbook refs: new Bird, Hudak |
68 Adjust FP textbook refs: new Bird, Hudak |
68 Discrete math textbook: Rosen? |
69 Discrete math textbook: Rosen? |
69 |
|
70 say something about "abbreviations" when defs are introduced. |
|
71 |
70 |
72 adjust type of ^ in tab:overloading |
71 adjust type of ^ in tab:overloading |
73 |
72 |
74 an example of induction: !y. A --> B --> C ?? |
73 an example of induction: !y. A --> B --> C ?? |
75 |
74 |