src/Pure/Thy/thm_deps.ML
2012-09-25 wenzelm 2012-09-25 separate module Graph_Display; tuned signature;
2011-08-20 wenzelm 2011-08-20 reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;
2011-08-20 wenzelm 2011-08-20 clarified fulfill_norm_proof: no join_thms yet; clarified priority of fulfill_proof_future, which is followed by explicit join_thms; explicit Thm.future_body_of without join yet; tuned Thm.future_result: join_promises without fulfill_norm_proof;
2011-04-26 wenzelm 2011-04-26 mark thm tag "kind" as legacy;
2011-01-15 berghofe 2011-01-15 unused_thms no longer compares propositions, since this is no longer needed and did not work properly any longer after the addition of class constraints to propositions.
2011-01-10 wenzelm 2011-01-10 standardized split_last/last_elem towards List.last; eliminated obsolete Library.last_elem;
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-07-21 wenzelm 2010-07-21 thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
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;
2009-11-19 wenzelm 2009-11-19 unused_thms: show only results from 'theorem(s)' package (via old-style kinds); misc tuning -- slightly less hermetic names;
2009-11-12 wenzelm 2009-11-12 unused_thms: ignore kind -- already observes "concealed" flag;
2009-11-02 wenzelm 2009-11-02 structure Thm_Deps;
2009-10-25 wenzelm 2009-10-25 maintain group via name space, not tags; tuned;
2009-10-01 wenzelm 2009-10-01 back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
2009-09-28 wenzelm 2009-09-28 fold_body_thms: pass pthm identifier; fold_body_thms: dismiss path-etic attempt to check for cycles (cf. e24acd21e60e) -- could be masked by "seen"; fulfill_proof/thm_proof: check for thm cycles at the substitution point;
2009-05-18 haftmann 2009-05-18 introduced Thm.generatedK
2009-05-16 bulwahn 2009-05-16 added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-11-17 wenzelm 2008-11-17 simplified thm_deps -- no need to build a graph datastructure;
2008-11-16 wenzelm 2008-11-16 proof_body/pthm: removed redundant types field;
2008-11-16 wenzelm 2008-11-16 clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-15 wenzelm 2008-11-15 retrieve thm deps from proof_body; removed obsolete enable/disable operation;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-04-17 wenzelm 2008-04-17 unused_thms: sort_distinct;
2008-04-16 wenzelm 2008-04-16 removed obsolete BASIC_THM_DEPS; unused_thms: simplified signature, use proper PureThy.facts_of; misc tuning;
2008-02-28 berghofe 2008-02-28 Added function for finding unused theorems.
2008-02-25 wenzelm 2008-02-25 thm_deps: sort result;
2007-09-08 wenzelm 2007-09-08 Present.session_name;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-09-18 wenzelm 2006-09-18 Present.display_graph;
2006-01-27 wenzelm 2006-01-27 moved theorem tags from Drule to PureThy;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-03 berghofe 2005-08-03 Adapted to new argument format of MinProof constructor.
2005-07-19 wenzelm 2005-07-19 Inttab.defined;
2005-06-05 wenzelm 2005-06-05 File.isatool, File.shell_path;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2002-08-27 wenzelm 2002-08-27 Thm.proof_of;
2001-11-19 berghofe 2001-11-19 Now handles different theorems with same name more gracefully.
2001-10-17 wenzelm 2001-10-17 tuned comments;
2001-09-28 berghofe 2001-09-28 Exchanged % and %%.
2001-09-01 wenzelm 2001-09-01 renamed `keep_derivs' to `proofs', and made an integer;
2001-08-31 berghofe 2001-08-31 Adapted to new proof terms.
2000-08-02 wenzelm 2000-08-02 adapted deriv;
2000-07-27 wenzelm 2000-07-27 tuned;
1999-10-13 wenzelm 1999-10-13 system;
1999-10-07 berghofe 1999-10-07 Replaced update_new by update.
1999-10-07 berghofe 1999-10-07 Added functions for enabling and disabling derivations.
1999-10-07 wenzelm 1999-10-07 $ISATOOL;
1999-10-07 berghofe 1999-10-07 New function thm_deps for visualizing dependencies of theorems.