equal
deleted
inserted
replaced
71 behaviour is analogous to 'for' in attributes "where" and "of". |
71 behaviour is analogous to 'for' in attributes "where" and "of". |
72 Configuration option rule_insts_schematic (default false) controls use |
72 Configuration option rule_insts_schematic (default false) controls use |
73 of schematic variables outside the context. Minor INCOMPATIBILITY, |
73 of schematic variables outside the context. Minor INCOMPATIBILITY, |
74 declare rule_insts_schematic = true temporarily and update to use local |
74 declare rule_insts_schematic = true temporarily and update to use local |
75 variable declarations or dummy patterns instead. |
75 variable declarations or dummy patterns instead. |
76 |
|
77 * Configuration option "rule_insts_schematic" determines whether proof |
|
78 methods like "rule_tac" may refer to undeclared schematic variables |
|
79 implicitly, instead of using proper 'for' declarations. This historic |
|
80 behaviour is still the default for some time. |
|
81 |
76 |
82 * Command "class_deps" takes optional sort arguments constraining |
77 * Command "class_deps" takes optional sort arguments constraining |
83 the search space. |
78 the search space. |
84 |
79 |
85 * Lexical separation of signed and unsigend numerals: categories "num" |
80 * Lexical separation of signed and unsigend numerals: categories "num" |