src/Pure/Thy/thm_database.ML
2007-07-23 wenzelm 2007-07-23 added compatibility file for ML systems without multithreading;
2007-01-21 wenzelm 2007-01-21 use_text: added name argument;
2007-01-19 wenzelm 2007-01-19 moved ML context stuff to from Context to ML_Context;
2007-01-19 wenzelm 2007-01-19 adapted ML context operations;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-11-23 wenzelm 2006-11-23 moved ML identifiers to structure ML_Syntax;
2006-10-09 wenzelm 2006-10-09 moved Context.ml_output to Output.ml_output;
2006-09-21 wenzelm 2006-09-21 added is_ml_reserved;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-02-11 wenzelm 2006-02-11 tuned;
2006-02-06 wenzelm 2006-02-06 TableFun: renamed xxx_multi to xxx_list;
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-28 wenzelm 2005-08-28 added (use_)legacy_bindings;
2005-04-23 wenzelm 2005-04-23 tuned comment;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-04-26 wenzelm 2004-04-26 use Syntax.is_ascii_identifier;
2002-07-02 wenzelm 2002-07-02 removed thms_containing (see pure_thy.ML and proof_context.ML);
2001-10-22 wenzelm 2001-10-22 moved goal related stuff to goals.ML;
2001-10-14 wenzelm 2001-10-14 added qed_spec_mp etc.;
2001-08-31 berghofe 2001-08-31 Exported ml_reserved.
2001-02-01 wenzelm 2001-02-01 thms_containing: term args;
2001-01-16 wenzelm 2001-01-16 use_text etc.: proper output of error messages;
2001-01-12 wenzelm 2001-01-12 use_text_verbose: priority output;
1999-12-07 nipkow 1999-12-07 Fixed bug in find-functions: list of parameters must be reversed before subsitution.
1999-10-13 wenzelm 1999-10-13 use_text_verbose;
1999-10-05 wenzelm 1999-10-05 fixed ml_store_thm(s): deriv;
1999-09-26 wenzelm 1999-09-26 added print_thms_containing;
1999-09-22 wenzelm 1999-09-22 ml_store_thm: no warning for "";
1999-09-03 wenzelm 1999-09-03 added no_qed;
1999-09-01 wenzelm 1999-09-01 added store/bind_thms;
1999-08-06 paulson 1999-08-06 now catches exn THEORY and prints an error message
1999-03-09 wenzelm 1999-03-09 Present.theorem;
1999-02-03 wenzelm 1999-02-03 open BasicThmDatabase; Present.thm;
1998-10-23 wenzelm 1998-10-23 export is_ml_identifier;
1998-08-20 paulson 1998-08-20 Now qed_spec_mp respects locales, by calling ml_store_thm instead of bind_thm
1998-07-17 paulson 1998-07-17 added comments
1998-06-29 wenzelm 1998-06-29 use_text: verbose flag;
1998-06-15 wenzelm 1998-06-15 use_text replaces use_strings;
1998-01-09 wenzelm 1998-01-09 thm_ord;
1998-01-08 wenzelm 1998-01-08 fixed thm_less;
1997-12-19 wenzelm 1997-12-19 adapted to new sort function;
1997-11-26 wenzelm 1997-11-26 fixed type of thms_containing;
1997-10-30 wenzelm 1997-10-30 tuned;
1997-10-28 wenzelm 1997-10-28 restructured -- uses PureThy storage facilities;
1997-10-24 wenzelm 1997-10-24 ProtoPure.flexpair_def;
1997-10-23 wenzelm 1997-10-23 tuned;
1997-08-06 wenzelm 1997-08-06 renamed use_string to use_strings;
1997-08-06 wenzelm 1997-08-06 tuned names;
1997-08-06 berghofe 1997-08-06 Moved "qed" - functions etc. from thy_read.ML to thm_database.ML.
1996-11-01 paulson 1996-11-01 Replaced "sum" (only usage?) by foldl op+
1996-05-17 nipkow 1996-05-17 Added missing default clause | top_const _ = None;
1996-04-09 berghofe 1996-04-09 select_match now sorts list of matching theorems according to the number of premises and size of the required substitution
1996-03-15 berghofe 1996-03-15 Added some functions which allow redirection of Isabelle's output
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1995-10-25 clasohm 1995-10-25 removed "duplicate" warning from store_thm_db; changed place where store_thm_db is called for a theory's axioms
1995-10-06 clasohm 1995-10-06 changed some comments
1995-10-04 clasohm 1995-10-04 added removal of theorems if theory is to be reloaded; changed functions for local simpsets
1995-09-01 clasohm 1995-09-01 fixed bug: duplicate "duplicate" warnings