src/Pure/Isar/obtain.ML
2000-07-30 wenzelm 2000-07-30 turned into plain context element; exporter setup;
2000-07-13 wenzelm 2000-07-13 bind_skolem;
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-03-30 wenzelm 2000-03-30 ProofContext.find_free;
2000-03-21 wenzelm 2000-03-21 handle general case: params and hyps of thesis;
2000-01-06 wenzelm 2000-01-06 obtain: renamed 'in' to 'where';
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.