src/Pure/Isar/obtain.ML
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;
2011-11-03 ago tuned signature -- canonical argument order;
2011-06-09 ago discontinued Name.variant to emphasize that this is old-style / indirect;
2011-04-28 ago eliminated slightly odd Proof_Context.bind_fixes;
2011-04-27 ago more precise positions via binding;
2011-04-27 ago clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
2011-04-27 ago tuned signature -- eliminated odd comment;
2011-04-27 ago more formal treatment of parameters, avoiding slightly odd Variable.intern_fixed;
2011-04-27 ago reorganized fixes as specialized (global) name space;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago tuned signature, disentangled dependencies;
2011-04-08 ago explicit structure Syntax_Trans;
2010-12-17 ago renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-09-05 ago turned show_sorts/show_types into proper configuration options;
2010-08-30 ago tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
2010-04-25 ago modernized naming conventions of main Isar proof elements;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-07 ago modernized structure Object_Logic;
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-11-02 ago modernized structure Proof_Display;
2009-11-02 ago modernized structure AutoBind;
2009-11-01 ago modernized structure Context_Rules;
2009-11-01 ago modernized structure Rule_Cases;
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-09-30 ago eliminated dead code;
2009-07-26 ago Variable.focus: named parameters;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-03-28 ago renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 ago replaced add_binds(_i) by bind_terms -- internal version only;
2009-03-19 ago use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago 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;
2009-03-03 ago Thm.binding;
2009-01-21 ago binding is alias for Binding.T
2009-01-07 ago qed/after_qed: singleton result;
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-09-02 ago type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-04-03 ago renamed Variable.import to import_thms (avoid clash with Alice keywords);
2006-12-06 ago export: added explicit term operation;
2006-11-30 ago qualified MetaSimplifier.norm_hhf(_protect);
2006-11-07 ago moved statement to specification.ML;
2006-09-30 ago statement: Variable.fix_frees;
2006-08-02 ago added tactical result;
2006-07-27 ago moved basic assumption operations from structure ProofContext to Assumption;
2006-07-26 ago Variable.import(T): result includes fixed types/terms;
2006-07-25 ago added find_free (from term.ML);
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-07-04 ago guess: proper context for polymorphic parameters;