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-03-28 clasohm 1995-03-28 changed string scanner so that newlines ('\n') are allowed and ignored inside strings
1994-11-14 clasohm 1994-11-14 added check for newlines not enclosed by '\' inside strings
1994-05-19 wenzelm 1994-05-19 (replaces Thy/scan.ML) scanner now based on combinators of structure Scanner; improved handling of keywords; now supports long.ids, (* (* nested *) comments *), {| verbatim text |};