src/Pure/Thy/syntax.ML
1994-02-03 wenzelm 1994-02-03 syntax for type abbreviations;
1993-12-21 nipkow 1993-12-21 Added []-field to extend_theory to accomodate type abbreviations.
1993-11-16 clasohm 1993-11-16 moved call of store_theory to end of use t.thy; use t.ML; use_thy now needs the exact theory name (capital/lower letters); improved handling of incompletly read theories; added function unlink_thy, removed function relations; added reference variable delete_tmpfile; removed some bugs
1993-10-26 clasohm 1993-10-26 corrected some spelling mistakes; removed a bug that made it impossible to read theories that don't have a ML file; extended syntax for bases in syntax.ML: a string can be used to specify a theory that is to be read but is not merged into the base (useful for pseudo theories used to document the dependencies of ML files)
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-10-04 wenzelm 1993-10-04 Pure/Thy/syntax.ML removed {parse,print}_{pre,post}_proc; removed 'val ax = ..';
1993-09-16 clasohm 1993-09-16 Initial revision