src/Pure/Isar/obtain.ML
2005-07-14 wenzelm 2005-07-14 tuned;
2005-07-13 haftmann 2005-07-13 (intermediate commit)
2005-06-29 wenzelm 2005-06-29 no Syntax.internal on thesis;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2002-02-27 wenzelm 2002-02-27 improved messages;
2001-12-06 wenzelm 2001-12-06 Syntax.internal thesis;
2001-12-03 wenzelm 2001-12-03 renamed rule_context.ML to context_rules.ML;
2001-11-29 wenzelm 2001-11-29 RuleContext.intro_query_local;
2001-11-11 wenzelm 2001-11-11 Proof.have_i: multiple statements;
2001-11-05 wenzelm 2001-11-05 pretty/print functions with context;
2001-10-22 wenzelm 2001-10-22 improved source arrangement of obtain;
2001-10-16 wenzelm 2001-10-16 simplified exporter interface;
2001-10-14 wenzelm 2001-10-14 use ObjectLogic;
2001-02-01 wenzelm 2001-02-01 comment
2000-12-04 wenzelm 2000-12-04 fixed binding of parameters;
2000-11-13 wenzelm 2000-11-13 tuned statement args;
2000-11-03 wenzelm 2000-11-03 improved handling of "that": insert into goal, only declare as Pure "intro"; eliminated functor;
2000-07-31 wenzelm 2000-07-31 tuned;
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.