equal
deleted
inserted
replaced
54 that the result needs to be unique, which means fact specifications |
54 that the result needs to be unique, which means fact specifications |
55 may have to be refined after enriching a proof context. |
55 may have to be refined after enriching a proof context. |
56 |
56 |
57 * Isabelle/Isar reference manual provides more formal references in |
57 * Isabelle/Isar reference manual provides more formal references in |
58 syntax diagrams. |
58 syntax diagrams. |
|
59 |
|
60 * Attribute case_names has been refined: the assumptions in each case can |
|
61 be named now by following the case name with [name1 name2 ...]. |
59 |
62 |
60 |
63 |
61 *** HOL *** |
64 *** HOL *** |
62 |
65 |
63 * Classes bot and top require underlying partial order rather than preorder: |
66 * Classes bot and top require underlying partial order rather than preorder: |