changeset 11021 | 41de937d338b |
parent 10582 | 49ebade930ea |
child 11764 | fd780dd6e0b4 |
--- a/src/Pure/Isar/obtain.ML Thu Feb 01 20:44:19 2001 +0100 +++ b/src/Pure/Isar/obtain.ML Thu Feb 01 20:45:11 2001 +0100 @@ -11,7 +11,7 @@ { fix thesis - assume that: "!!x. P x ==> thesis" + assume that [intro]: "!!x. P x ==> thesis" <chain_facts> have thesis <proof (insert that)> } fix x assm (obtained) "P x"