src/Pure/Isar/obtain.ML
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-15 wenzelm 2006-01-15 guess: used fixed inferred_type of vars;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-13 wenzelm 2006-01-13 uniform handling of fixes;
2006-01-10 wenzelm 2006-01-10 generic attributes;
2005-11-16 wenzelm 2005-11-16 Term.betapplys;
2005-11-10 wenzelm 2005-11-10 guess: Seq.hd; Term.find_free;
2005-11-08 wenzelm 2005-11-08 simplified after_qed;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-21 wenzelm 2005-10-21 improved check_result; Goal.init, Goal.conclude;
2005-10-18 wenzelm 2005-10-18 tuned error msg; tuned;
2005-10-15 wenzelm 2005-10-15 added 'guess', which derives the obtained context from the course of reasoning;
2005-09-13 wenzelm 2005-09-13 tuned Isar proof elements;
2005-08-18 wenzelm 2005-08-18 prepare attributes here; tuned;
2005-08-08 ballarin 2005-08-08 After_qed takes result argument.
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.