equal
deleted
inserted
replaced
22 have result: "C x y" |
22 have result: "C x y" |
23 if "A x" and "B y" |
23 if "A x" and "B y" |
24 for x :: 'a and y :: 'a |
24 for x :: 'a and y :: 'a |
25 <proof> |
25 <proof> |
26 |
26 |
27 The local assumptions are always bound to the name "prems". The result |
27 The local assumptions are bound to the name "that". The result is |
28 is exported from context of the statement as usual. The above roughly |
28 exported from context of the statement as usual. The above roughly |
29 corresponds to a raw proof block like this: |
29 corresponds to a raw proof block like this: |
30 |
30 |
31 { |
31 { |
32 fix x :: 'a and y :: 'a |
32 fix x :: 'a and y :: 'a |
33 assume prems: "A x" "B y" |
33 assume that: "A x" "B y" |
34 have "C x y" <proof> |
34 have "C x y" <proof> |
35 } |
35 } |
36 note result = this |
36 note result = this |
37 |
37 |
38 * New command 'supply' supports fact definitions during goal refinement |
38 * New command 'supply' supports fact definitions during goal refinement |