equal
deleted
inserted
replaced
153 |
153 |
154 * Term abbreviations via 'is' patterns also work for schematic |
154 * Term abbreviations via 'is' patterns also work for schematic |
155 statements: result is abstracted over unknowns. |
155 statements: result is abstracted over unknowns. |
156 |
156 |
157 * Local goals ('have', 'show', 'hence', 'thus') allow structured |
157 * Local goals ('have', 'show', 'hence', 'thus') allow structured |
158 statements like fixes/assumes/shows in theorem specifications, but the |
158 rule statements like fixes/assumes/shows in theorem specifications, but |
159 notation is postfix with keywords 'if' (or 'when') and 'for'. For |
159 the notation is postfix with keywords 'if' (or 'when') and 'for'. For |
160 example: |
160 example: |
161 |
161 |
162 have result: "C x y" |
162 have result: "C x y" |
163 if "A x" and "B y" |
163 if "A x" and "B y" |
164 for x :: 'a and y :: 'a |
164 for x :: 'a and y :: 'a |
176 note result = this |
176 note result = this |
177 |
177 |
178 The keyword 'when' may be used instead of 'if', to indicate 'presume' |
178 The keyword 'when' may be used instead of 'if', to indicate 'presume' |
179 instead of 'assume' above. |
179 instead of 'assume' above. |
180 |
180 |
181 * Assumptions ('assume', 'presume') allow structured statements using |
181 * Assumptions ('assume', 'presume') allow structured rule statements |
182 'if' and 'for', similar to 'have' etc. above. For example: |
182 using 'if' and 'for', similar to 'have' etc. above. For example: |
183 |
183 |
184 assume result: "C x y" |
184 assume result: "C x y" |
185 if "A x" and "B y" |
185 if "A x" and "B y" |
186 for x :: 'a and y :: 'a |
186 for x :: 'a and y :: 'a |
187 |
187 |