src/Pure/Proof/extraction.ML
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;
2008-06-18 wenzelm 2008-06-18 OldGoals.simple_read_term;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-15 wenzelm 2008-04-15 Thm.forall_elim_var(s);
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-29 wenzelm 2008-03-29 simplified PureThy.store_thm;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;