| changeset 11021 | 41de937d338b |
| parent 10582 | 49ebade930ea |
| child 11764 | fd780dd6e0b4 |
| 11020:646c929b6293 | 11021:41de937d338b |
|---|---|
9 <chain_facts> |
9 <chain_facts> |
10 obtain x where "P x" <proof> == |
10 obtain x where "P x" <proof> == |
11 |
11 |
12 { |
12 { |
13 fix thesis |
13 fix thesis |
14 assume that: "!!x. P x ==> thesis" |
14 assume that [intro]: "!!x. P x ==> thesis" |
15 <chain_facts> have thesis <proof (insert that)> |
15 <chain_facts> have thesis <proof (insert that)> |
16 } |
16 } |
17 fix x assm (obtained) "P x" |
17 fix x assm (obtained) "P x" |
18 |
18 |
19 *) |
19 *) |