# HG changeset patch
# User wenzelm
# Date 1113410863 -7200
# Node ID dfa913c68f9d14d08e71887a66d80f8055be47f4
# Parent  9b8da47715c39b0158c5606104ca99fca96d84ce
*** MESSAGE REFERS TO PREVIOUS VERSION ***
added datatype interval, improved thm selections;

diff -r 9b8da47715c3 -r dfa913c68f9d src/Pure/pure_thy.ML
--- 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;
+