summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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 |