src/Pure/Proof/extraction.ML
2016-06-06 haftmann 2016-06-06 explicit tagging of code equations de-baroquifies interface
2016-04-12 wenzelm 2016-04-12 Type_Infer.object_logic controls improvement of type inference result;
2016-04-09 wenzelm 2016-04-09 clarified context; avoid Unsynchronized.ref;
2015-12-19 wenzelm 2015-12-19 tuned signature;
2015-09-02 wenzelm 2015-09-02 trim context for persistent storage; clarified thm equality;
2015-08-28 wenzelm 2015-08-28 tuned signature;
2015-07-28 wenzelm 2015-07-28 clarified context;
2015-03-23 wenzelm 2015-03-23 local fixes may depend on goal params;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete Output.urgent_message;
2014-09-24 haftmann 2014-09-24 tuned
2014-04-06 wenzelm 2014-04-06 more source positions;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-18 wenzelm 2014-03-18 clarified module arrangement; more antiquotations;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2012-10-21 haftmann 2012-10-21 more conventional argument order; dropped dead code
2012-08-07 wenzelm 2012-08-07 tuned signature -- make Pretty less dependent on Symbol;
2012-08-02 wenzelm 2012-08-02 more official command specifications, including source position;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-13 wenzelm 2012-03-13 more explicit indication of def names;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2011-08-08 wenzelm 2011-08-08 modernized strcture Proof_Checker;
2011-04-19 wenzelm 2011-04-19 prefer internal types, via Simple_Syntax.read_typ;
2011-04-19 wenzelm 2011-04-19 eliminated obsolete Proof_Syntax.strip_sorts_consttypes;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-12-01 wenzelm 2010-12-01 more direct use of binder_types/body_type;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-08-26 wenzelm 2010-08-26 theory data merge: prefer left side uniformly;
2010-06-03 wenzelm 2010-06-03 do not open Proofterm, which is very ould style;
2010-06-01 berghofe 2010-06-01 Renamed TypeInfer to Type_Infer.
2010-06-01 berghofe 2010-06-01 Adapted to new format of proof terms containing explicit proofs of class membership.
2010-05-15 wenzelm 2010-05-15 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-05-08 wenzelm 2010-05-08 renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
2010-05-04 wenzelm 2010-05-04 simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
2010-03-30 krauss 2010-03-30 switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
2010-03-27 wenzelm 2010-03-27 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML); discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def; modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;
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-02 wenzelm 2010-03-02 more precise scope of exception handler;
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-21 wenzelm 2009-11-21 explicitly mark some legacy freeze operations;
2009-11-15 wenzelm 2009-11-15 add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature; explicit extraction_expand vs. extraction_expand_def attribute;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Syntax;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 eliminated some old folds;
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir.subst_XXX;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir operations;