src/Pure/Isar/obtain.ML
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-05 wenzelm 2015-03-05 tuned -- more explicit use of context;
2015-03-01 wenzelm 2015-03-01 added Proof_Context.cterm_of/ctyp_of convenience;
2014-05-09 wenzelm 2014-05-09 more position markup to help locating the query context, e.g. from "Info" dockable;
2014-05-07 wenzelm 2014-05-07 print results as "state", to avoid intrusion into the source text; print new local theory (again);
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-06-26 wenzelm 2013-06-26 tuned signature;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-09-29 wenzelm 2012-09-29 more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-04-27 wenzelm 2012-04-27 clarified signature;
2012-02-28 wenzelm 2012-02-28 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_all_free in favour of plain Logic.all;
2011-11-07 wenzelm 2011-11-07 tuned signature -- avoid spurious Thm.mixed_attribute;
2011-11-03 wenzelm 2011-11-03 more general Proof_Context.bind_propp, which allows outer parameters; obtain: some support for term bindings within the proof, depending on parameters;
2011-11-03 wenzelm 2011-11-03 tuned signature;
2011-11-03 wenzelm 2011-11-03 tuned signature -- canonical argument order;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-04-28 wenzelm 2011-04-28 eliminated slightly odd Proof_Context.bind_fixes; tuned;
2011-04-27 wenzelm 2011-04-27 more precise positions via binding;
2011-04-27 wenzelm 2011-04-27 clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
2011-04-27 wenzelm 2011-04-27 tuned signature -- eliminated odd comment;
2011-04-27 wenzelm 2011-04-27 more formal treatment of parameters, avoiding slightly odd Variable.intern_fixed;
2011-04-27 wenzelm 2011-04-27 reorganized fixes as specialized (global) name space;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 tuned signature, disentangled dependencies;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-08-30 wenzelm 2010-08-30 tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Display;
2009-11-02 wenzelm 2009-11-02 modernized structure AutoBind;
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-09-30 wenzelm 2009-09-30 eliminated dead code;
2009-07-26 wenzelm 2009-07-26 Variable.focus: named parameters;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-24 wenzelm 2009-06-24 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 replaced add_binds(_i) by bind_terms -- internal version only;
2009-03-19 wenzelm 2009-03-19 use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-03 wenzelm 2009-03-03 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify; minor tuning;
2009-03-03 wenzelm 2009-03-03 Thm.binding;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2009-01-07 wenzelm 2009-01-07 qed/after_qed: singleton result;
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements; simplified ProofContext.inferred_param;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-04-03 wenzelm 2007-04-03 renamed Variable.import to import_thms (avoid clash with Alice keywords);
2006-12-06 wenzelm 2006-12-06 export: added explicit term operation;