author | wenzelm |
Fri, 01 Oct 1999 20:38:16 +0200 | |
changeset 7677 | de2e468a42c8 |
parent 7676 | 811022c3837e |
child 7678 | 027b6ec2f084 |
--- 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: