nipkow [Tue, 24 May 1994 09:04:03 +0200] rev 394
Modified mk_meta_eq to leave meta-equlities on unchanged.
Thus you may now add ==-thms to simpsets.
wenzelm [Thu, 19 May 1994 17:06:24 +0200] rev 393
thy reader now initialised by init_thy_reader();
wenzelm [Thu, 19 May 1994 16:42:04 +0200] rev 392
*** empty log message ***
wenzelm [Thu, 19 May 1994 16:30:56 +0200] rev 391
(was Thy/read.ML)
minor changes to accomodate new ThyScan and ThyParse;
wenzelm [Thu, 19 May 1994 16:27:16 +0200] rev 390
*** empty log message ***
wenzelm [Thu, 19 May 1994 16:26:19 +0200] rev 389
(replaces Thy/parse.ML and Thy/syntax.ML)
much simpler because of new theory extension functions;
theory is now built up from an arbitrary list of definable 'sections';
new axclass and instance sections;
wenzelm [Thu, 19 May 1994 16:25:03 +0200] rev 388
(replaces Thy/scan.ML)
scanner now based on combinators of structure Scanner;
improved handling of keywords;
now supports long.ids, (* (* nested *) comments *), {| verbatim text |};