changeset 7677 | de2e468a42c8 |
parent 7674 | 99305245f6bd |
child 7923 | 895d31b54da5 |
--- a/src/Pure/Isar/obtain.ML Fri Oct 01 20:38:00 1999 +0200 +++ b/src/Pure/Isar/obtain.ML Fri Oct 01 20:38:16 1999 +0200 @@ -3,7 +3,7 @@ Author: Markus Wenzel, TU Muenchen The 'obtain' language element -- achieves (eliminated) existential -quantification proof command level. +quantification at proof command level. The common case: