2016-04-26 ago 'obtain' supports structured statements (similar to 'define');
2016-04-26 ago more uniform operations for structured statements;
2016-04-26 ago defs are closed, which leads to proper auto_bind_facts;
2016-04-24 ago clarified modules;
2016-04-18 ago prefer internal attribute source;
2015-12-13 ago more general types Proof.method / context_tactic;
2015-11-13 ago support for structure statements in 'assume', 'presume';
2015-09-25 ago moved remaining display.ML to more_thm.ML;
2015-08-16 ago added Thm.chyps_of;
2015-07-08 ago Variable.focus etc.: optional bindings provided by user;
2015-07-05 ago simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-06-22 ago support 'when' statement, which corresponds to 'presume';
2015-06-15 ago more robust: variables need not occur in body;
2015-06-14 ago improved treatment of Element.Obtains via Expression.prepare_stmt;
2015-06-14 ago tuned comment;
2015-06-13 ago tuned signature;
2015-06-13 ago open parameters for 'consider' rule;
2015-06-13 ago eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
2015-06-13 ago clarified 'obtain', using structured 'have' statement;
2015-06-13 ago tuned comments;
2015-06-13 ago clarified 'consider', using structured 'have' statement;
2015-06-11 ago support for 'consider' command;
2015-06-11 ago support to parse obtain clause without type-checking yet;
2015-06-11 ago tuned signature;
2015-06-10 ago clarified local after_qed: result is not exported yet;
2015-06-10 ago support for "if prems" in local goal statements;
2015-06-09 ago more uniform treatment of auto bindings vs. explicit user bindings;
2015-06-09 ago tuned signature;
2015-06-09 ago allow for_fixes for 'have', 'show' etc.;
2015-06-09 ago clarified abstracted term bindings (again, see c8384ff11711);
2015-06-09 ago clarified term bindings;
2015-06-08 ago clarified context;
2015-06-08 ago tuned;
2015-06-08 ago clarified abstracted term bindings;
2015-06-08 ago avoid duplicate warning due to Variable.warn_extra_tfrees;
2015-06-08 ago clarified Proof_Context.cert_propp/read_propp;
2015-06-08 ago more careful treatment of term bindings in 'obtain' proof body;
2015-06-07 ago tuned signature;
2015-06-07 ago tuned signature;
2015-06-07 ago tuned signature;
2015-06-07 ago tuned signature;
2015-05-30 ago more explicit context;
2015-04-08 ago proper context for Object_Logic operations;
2015-03-06 ago clarified context;
2015-03-06 ago Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-05 ago tuned -- more explicit use of context;
2015-03-01 ago added Proof_Context.cterm_of/ctyp_of convenience;
2014-05-09 ago more position markup to help locating the query context, e.g. from "Info" dockable;
2014-05-07 ago print results as "state", to avoid intrusion into the source text;
2013-12-31 ago proper context for norm_hhf and derived operations;
2013-06-26 ago tuned signature;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-09-29 ago more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-04-27 ago clarified signature;
2012-02-28 ago display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
2012-01-14 ago discontinued old-style Term.list_abs in favour of plain Term.abs;
2012-01-14 ago discontinued old-style Term.list_all_free in favour of plain Logic.all;
2011-11-07 ago tuned signature -- avoid spurious Thm.mixed_attribute;
2011-11-03 ago more general Proof_Context.bind_propp, which allows outer parameters;
2011-11-03 ago tuned signature;