equal
deleted
inserted
replaced
64 statement. |
64 statement. |
65 |
65 |
66 |
66 |
67 *** Isar *** |
67 *** Isar *** |
68 |
68 |
69 * Many specification elements support structured statements with 'if' |
69 * Command 'axiomatization' has become more restrictive to correspond |
70 eigen-context, e.g. 'axiomatization', 'definition', 'inductive', |
70 better to internal axioms as singleton facts with mandatory name. Minor |
71 'function'. |
71 INCOMPATIBILITY. |
|
72 |
|
73 * Many specification elements support structured statements with 'if' / |
|
74 'for' eigen-context, e.g. 'axiomatization', 'abbreviation', |
|
75 'definition', 'inductive', 'function'. |
72 |
76 |
73 * Toplevel theorem statements support eigen-context notation with 'if' / |
77 * Toplevel theorem statements support eigen-context notation with 'if' / |
74 'for' (in postix), which corresponds to 'assumes' / 'fixes' in the |
78 'for' (in postix), which corresponds to 'assumes' / 'fixes' in the |
75 traditional long statement form (in prefix). Local premises are called |
79 traditional long statement form (in prefix). Local premises are called |
76 "that" or "assms", respectively. Empty premises are *not* bound in the |
80 "that" or "assms", respectively. Empty premises are *not* bound in the |