equal
deleted
inserted
replaced
56 established at the end of a proof are properly identified in the theorem |
56 established at the end of a proof are properly identified in the theorem |
57 statement. |
57 statement. |
58 |
58 |
59 |
59 |
60 *** Isar *** |
60 *** Isar *** |
|
61 |
|
62 * Many specification elements support structured statements with 'if' |
|
63 eigen-context, e.g. 'axiomatization', 'definition', 'inductive', |
|
64 'function'. |
61 |
65 |
62 * Command 'define' introduces a local (non-polymorphic) definition, with |
66 * Command 'define' introduces a local (non-polymorphic) definition, with |
63 optional abstraction over local parameters. The syntax resembles |
67 optional abstraction over local parameters. The syntax resembles |
64 'definition' and 'obtain'. It fits better into the Isar language than |
68 'definition' and 'obtain'. It fits better into the Isar language than |
65 old 'def', which is now a legacy feature. |
69 old 'def', which is now a legacy feature. |