equal
deleted
inserted
replaced
52 page 157 display: Union operator is too big |
52 page 157 display: Union operator is too big |
53 |
53 |
54 page 158, "!": Isabelle now permits more general left-hand sides, so called |
54 page 158, "!": Isabelle now permits more general left-hand sides, so called |
55 higher-order patterns. |
55 higher-order patterns. |
56 |
56 |
|
57 Classical reasoner |
|
58 |
|
59 page 176: The package also provides tactics slow_tac, slow_best_tac, depth_tac |
|
60 and deepen_tac. |
57 |
61 |
58 ISABELLE'S OBJECT-LOGICS |
62 ISABELLE'S OBJECT-LOGICS |
59 |
63 |
60 First-Order Logic |
64 First-Order Logic |
61 |
65 |
62 page 191: FOL_dup_cs is now deleted (use deepen_tac FOL_cs instead) |
66 pages 191, 196: FOL_dup_cs is now deleted (use deepen_tac FOL_cs instead) |
63 |
67 |
64 Zermelo-Fraenkel Set Theory |
68 Zermelo-Fraenkel Set Theory |
65 |
69 |
66 page 204: type i has class term, not (just) logic |
70 page 204: type i has class term, not (just) logic |
67 |
71 |