equal
deleted
inserted
replaced
60 *** Isar *** |
60 *** Isar *** |
61 |
61 |
62 * Many specification elements support structured statements with 'if' |
62 * Many specification elements support structured statements with 'if' |
63 eigen-context, e.g. 'axiomatization', 'definition', 'inductive', |
63 eigen-context, e.g. 'axiomatization', 'definition', 'inductive', |
64 'function'. |
64 'function'. |
|
65 |
|
66 * Toplevel theorem statements support eigen-context notation with 'if' / |
|
67 'for' (in postix), which corresponds to 'assumes' / 'fixes' in the |
|
68 traditional long statement form (in prefix). Local premises are called |
|
69 "that" or "assms", respectively. Empty premises are *not* bound in the |
|
70 context: INCOMPATIBILITY. |
65 |
71 |
66 * Command 'define' introduces a local (non-polymorphic) definition, with |
72 * Command 'define' introduces a local (non-polymorphic) definition, with |
67 optional abstraction over local parameters. The syntax resembles |
73 optional abstraction over local parameters. The syntax resembles |
68 'definition' and 'obtain'. It fits better into the Isar language than |
74 'definition' and 'obtain'. It fits better into the Isar language than |
69 old 'def', which is now a legacy feature. |
75 old 'def', which is now a legacy feature. |