1996-12-16 wenzelm 1996-12-16 added symbol_input.ML;
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.
1996-01-29 clasohm 1996-01-29 added facility to associate arbitrary data with theories
1995-11-21 clasohm 1995-11-21 index.html files are now made separatly for each subdirectory
1995-10-26 clasohm 1995-10-26 renamed chart00 and 00-chart to "index"
1995-10-24 clasohm 1995-10-24 added generation of HTML files to thy_read.ML; removed old HTML package
1995-10-04 clasohm 1995-10-04 changed usage of structure Simplifier
1995-09-01 clasohm 1995-09-01 added cleanup of global simpset to thy_read; replaced error by warning for duplicate names in theorem database
1995-08-07 nipkow 1995-08-07 Added findI, findEs, and findE.
1995-06-01 clasohm 1995-06-01 commented thms_unifying_with out; placed thm_db into signature again; placed structures ThmDB and Readthy into Pure again; changed init_thy_reader so that thm_db and loaded_thys are preserved (necessary e.g. for ZF)
1995-05-30 clasohm 1995-05-30 fixed bug: ThySynFun really shouldn't be deleted
1995-05-29 clasohm 1995-05-29 replaced "All" by "all" in ThmdbFUN's ignore parameter
1995-05-29 clasohm 1995-05-29 added theorem database which contains axioms and theorems indexed by the constants they contain
1995-04-28 nipkow 1995-04-28 Added functor f() = struct end to hide functors to save space.
1994-06-20 clasohm 1994-06-20 parse.ML and scan.ML are now replaced by thy_parse.ML and thy_scan.ML
1994-06-01 wenzelm 1994-06-01 removed garbage; adapted to new ThySyn (interface for 'user sections');
1994-05-19 wenzelm 1994-05-19 *** empty log message ***
1993-10-22 clasohm 1993-10-22 changes in Readthy: - reads needed base theories automatically - keeps a time stamp for all read files - update function - checks for cycles - path list that is searched for files - reads theories that are created in .ML files - etc.
1993-09-16 clasohm 1993-09-16 Initial revision