equal
deleted
inserted
replaced
58 * Less waste of vertical space via negative line spacing (see Global |
58 * Less waste of vertical space via negative line spacing (see Global |
59 Options / Text Area). |
59 Options / Text Area). |
60 |
60 |
61 |
61 |
62 *** Pure *** |
62 *** Pure *** |
|
63 |
|
64 * Proof methods with explicit instantiation ("rule_tac", "subgoal_tac" |
|
65 etc.) allow an optional context of local variables ('for' declaration): |
|
66 these variables become schematic in the instantiated theorem. This |
|
67 behaviour is analogous to 'for' in attributes "where" and "of". |
63 |
68 |
64 * Command "class_deps" takes optional sort arguments constraining |
69 * Command "class_deps" takes optional sort arguments constraining |
65 the search space. |
70 the search space. |
66 |
71 |
67 * Lexical separation of signed and unsigend numerals: categories "num" |
72 * Lexical separation of signed and unsigend numerals: categories "num" |