src/Pure/Proof/extraction.ML
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;
2009-03-25 wenzelm 2009-03-25 Proofterm.approximate_proof_body;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-11 wenzelm 2009-03-11 explicit Binding.qualified_name -- prevents implicitly qualified bstring;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-01-27 wenzelm 2009-01-27 proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-11-16 wenzelm 2008-11-16 clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-16 berghofe 2008-11-16 Frees in PThms are now quantified in the order of their appearance in the proposition as well, to make it compatible (again) with variable order used by forall_intr_frees.
2008-11-15 wenzelm 2008-11-15 Thm.proof_of returns proof_body; adapted PThm;
2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-09-26 haftmann 2008-09-26 removed obsolete name convention "func"
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-07-29 haftmann 2008-07-29 PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;