1999-09-22 ago ml_store_thm: no warning for "";
1999-09-03 ago added no_qed;
1999-09-01 ago added store/bind_thms;
1999-08-06 ago now catches exn THEORY and prints an error message
1999-03-09 ago Present.theorem;
1999-02-03 ago open BasicThmDatabase;
1998-10-23 ago export is_ml_identifier;
1998-08-20 ago Now qed_spec_mp respects locales, by calling ml_store_thm
1998-07-17 ago added comments
1998-06-29 ago use_text: verbose flag;
1998-06-15 ago use_text replaces use_strings;
1998-01-09 ago thm_ord;
1998-01-08 ago fixed thm_less;
1997-12-19 ago adapted to new sort function;
1997-11-26 ago fixed type of thms_containing;
1997-10-30 ago tuned;
1997-10-28 ago restructured -- uses PureThy storage facilities;
1997-10-24 ago ProtoPure.flexpair_def;
1997-10-23 ago tuned;
1997-08-06 ago renamed use_string to use_strings;
1997-08-06 ago tuned names;
1997-08-06 ago Moved "qed" - functions etc. from thy_read.ML to thm_database.ML.
1996-11-01 ago Replaced "sum" (only usage?) by foldl op+
1996-05-17 ago Added missing default clause | top_const _ = None;
1996-04-09 ago select_match now sorts list of matching theorems according to the
1996-03-15 ago Added some functions which allow redirection of Isabelle's output
1996-02-16 ago Elimination of fully-functorial style.
1995-10-25 ago removed "duplicate" warning from store_thm_db;
1995-10-06 ago changed some comments
1995-10-04 ago added removal of theorems if theory is to be reloaded; changed functions for
1995-09-01 ago fixed bug: duplicate "duplicate" warnings
1995-09-01 ago added cleanup of global simpset to thy_read;
1995-08-30 ago added check for duplicate theorems in theorem database;
1995-08-18 ago fixed bug in findI
1995-08-07 ago Added findI, findEs, and findE.
1995-06-01 ago commented thms_unifying_with out; placed thm_db into signature again;
1995-05-30 ago removed thm_num and thm_db from signature
1995-05-30 ago fixed bug in thms_containing; changed error/warning messages;
1995-05-29 ago changed error message in thms_containing
1995-05-29 ago added theorem database which contains axioms and theorems indexed by the