src/Pure/Isar/obtain.ML
2000-01-05 wenzelm 2000-01-05 ObtainFun; prepare vars / asms / pats only once;
1999-10-22 wenzelm 1999-10-22 warn_extra_tfrees;
1999-10-01 wenzelm 1999-10-01 tuned comment;
1999-10-01 wenzelm 1999-10-01 The 'obtain' language element -- achieves (eliminated) existential quantification proof command level.