*** MESSAGE REFERS TO PREVIOUS VERSION ***
added datatype interval, improved thm selections;
--- a/src/Pure/pure_thy.ML Wed Apr 13 18:47:01 2005 +0200
+++ b/src/Pure/pure_thy.ML Wed Apr 13 18:47:43 2005 +0200
@@ -629,3 +629,4 @@
structure BasicPureThy: BASIC_PURE_THY = PureThy;
open BasicPureThy;
+