equal
deleted
inserted
replaced
61 |
61 |
62 * Command 'define' introduces a local (non-polymorphic) definition, with |
62 * Command 'define' introduces a local (non-polymorphic) definition, with |
63 optional abstraction over local parameters. The syntax resembles |
63 optional abstraction over local parameters. The syntax resembles |
64 'definition' and 'obtain'. It fits better into the Isar language than |
64 'definition' and 'obtain'. It fits better into the Isar language than |
65 old 'def', which is now a legacy feature. |
65 old 'def', which is now a legacy feature. |
|
66 |
|
67 * Command 'obtain' supports structured statements with 'if' / 'for' |
|
68 context. |
66 |
69 |
67 * Command '\<proof>' is an alias for 'sorry', with different |
70 * Command '\<proof>' is an alias for 'sorry', with different |
68 typesetting. E.g. to produce proof holes in examples and documentation. |
71 typesetting. E.g. to produce proof holes in examples and documentation. |
69 |
72 |
70 * The old proof method "default" has been removed (legacy since |
73 * The old proof method "default" has been removed (legacy since |