# HG changeset patch
# User wenzelm
# Date 880997263 -3600
# Node ID 7fb8a0c4578a69278210f7d445880630dfd8f917
# Parent  b0acd74da01daed7711ddcfb63c6e7fb447b6122
open;

diff -r b0acd74da01d -r 7fb8a0c4578a src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Mon Dec 01 18:27:06 1997 +0100
+++ b/src/HOL/arith_data.ML	Mon Dec 01 18:27:43 1997 +0100
@@ -212,3 +212,6 @@
 
 
 end;
+
+
+open ArithData;