src/Pure/Isar/obtain.ML
2006-11-30 wenzelm 2006-11-30 qualified MetaSimplifier.norm_hhf(_protect);
2006-11-07 wenzelm 2006-11-07 moved statement to specification.ML;
2006-09-30 wenzelm 2006-09-30 statement: Variable.fix_frees;
2006-08-02 wenzelm 2006-08-02 added tactical result; simplified obtain_export: no Seq.seq, no lifting of result prems; tuned;
2006-07-27 wenzelm 2006-07-27 moved basic assumption operations from structure ProofContext to Assumption;
2006-07-26 wenzelm 2006-07-26 Variable.import(T): result includes fixed types/terms;
2006-07-25 wenzelm 2006-07-25 added find_free (from term.ML);
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list); Name.internal;
2006-07-04 wenzelm 2006-07-04 guess: proper context for polymorphic parameters; tuned;
2006-07-03 wenzelm 2006-07-03 obtain_export: Thm.generalize; guess: fixed handling of mixfixes of vars; tuned;
2006-06-17 wenzelm 2006-06-17 Term.internal;
2006-06-15 wenzelm 2006-06-15 ProofContext: moved variable operations to struct Variable;
2006-06-11 wenzelm 2006-06-11 fixes: include mixfix syntax;
2006-06-05 wenzelm 2006-06-05 guess: more careful about local polymorphism; guess: explicit term vars in statement (avoids warning);
2006-05-07 wenzelm 2006-05-07 removed 'concl is' patterns;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-03-21 wenzelm 2006-03-21 subtract (op =);
2006-02-02 wenzelm 2006-02-02 Proof.refine_insert; statements: always use Attrib.src;
2006-02-02 wenzelm 2006-02-02 obtain(_i): optional name for 'that'; added statement (cf. Locale.theorem);
2006-01-31 wenzelm 2006-01-31 tuned comments;
2006-01-24 wenzelm 2006-01-24 ProofContext.inferred_param;
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;