NEWS
changeset 63284 c20946f5b6fb
parent 63283 a59801b7f125
child 63290 9ac558ab0906
equal deleted inserted replaced
63283:a59801b7f125 63284:c20946f5b6fb
    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