| Thu, 19 May 1994 16:12:37 +0200 | wenzelm | added infix op also: 'a * ('a -> 'b) -> 'b; | changeset | files |
| Thu, 19 May 1994 14:06:37 +0200 | clasohm | use_thy now uses use_string instead of creating a temporary file | changeset | files |
| Thu, 19 May 1994 13:45:50 +0200 | clasohm | added use_string: string -> unit to execute ML commands passed in a string | changeset | files |
| Thu, 19 May 1994 13:13:27 +0200 | clasohm | lookaheads are now computed faster (during the grammar is built) | changeset | files |