author | wenzelm |
Sat, 17 Sep 2005 12:18:00 +0200 | |
changeset 17445 | 3c9c46b820f5 |
parent 17444 | a389e5892691 |
child 17446 | f869b73b71ec |
--- a/NEWS Sat Sep 17 11:49:29 2005 +0200 +++ b/NEWS Sat Sep 17 12:18:00 2005 +0200 @@ -673,6 +673,12 @@ the old version is still required for ML proof scripts. +*** Cube *** + +* Converted to Isar theory format; use locales instead of axiomatic +theories. + + *** ML *** * Pure/library.ML no longer defines its own option datatype, but uses