equal
deleted
inserted
replaced
9 |
9 |
10 |
10 |
11 INTRODUCTION TO ISABELLE |
11 INTRODUCTION TO ISABELLE |
12 |
12 |
13 Advanced Methods |
13 Advanced Methods |
|
14 |
|
15 page 46: the theory sections can appear in any order |
|
16 |
|
17 page 48: theories may now contain a separate definition part |
14 |
18 |
15 page 52, middle: the declaration "types bool,nat" should be "types bool nat" |
19 page 52, middle: the declaration "types bool,nat" should be "types bool nat" |
16 |
20 |
17 page 57, bottom: should be addsimps in |
21 page 57, bottom: should be addsimps in |
18 val add_ss = FOL_ss addrews [add_0, add_Suc] |
22 val add_ss = FOL_ss addrews [add_0, add_Suc] |
54 page 158, "!": Isabelle now permits more general left-hand sides, so called |
58 page 158, "!": Isabelle now permits more general left-hand sides, so called |
55 higher-order patterns. |
59 higher-order patterns. |
56 |
60 |
57 Classical reasoner |
61 Classical reasoner |
58 |
62 |
59 page 176: The package also provides tactics slow_tac, slow_best_tac, depth_tac |
63 page 176: Classical sets may specify a "wrapper tactical", which can be used |
60 and deepen_tac. |
64 to define addss. The package also provides tactics slow_tac, slow_best_tac, |
|
65 depth_tac and deepen_tac. |
61 |
66 |
62 ISABELLE'S OBJECT-LOGICS |
67 ISABELLE'S OBJECT-LOGICS |
63 |
68 |
64 First-Order Logic |
69 First-Order Logic |
65 |
70 |