equal
deleted
inserted
replaced
91 * Many specification elements support structured statements with 'if' / |
91 * Many specification elements support structured statements with 'if' / |
92 'for' eigen-context, e.g. 'axiomatization', 'abbreviation', |
92 'for' eigen-context, e.g. 'axiomatization', 'abbreviation', |
93 'definition', 'inductive', 'function'. |
93 'definition', 'inductive', 'function'. |
94 |
94 |
95 * Toplevel theorem statements support eigen-context notation with 'if' / |
95 * Toplevel theorem statements support eigen-context notation with 'if' / |
96 'for' (in postix), which corresponds to 'assumes' / 'fixes' in the |
96 'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the |
97 traditional long statement form (in prefix). Local premises are called |
97 traditional long statement form (in prefix). Local premises are called |
98 "that" or "assms", respectively. Empty premises are *not* bound in the |
98 "that" or "assms", respectively. Empty premises are *not* bound in the |
99 context: INCOMPATIBILITY. |
99 context: INCOMPATIBILITY. |
100 |
100 |
101 * Command 'define' introduces a local (non-polymorphic) definition, with |
101 * Command 'define' introduces a local (non-polymorphic) definition, with |