# HG changeset patch
# User wenzelm
# Date 1113410752 -7200
# Node ID 80b421d8a8be2b8e01852abafd046a505614c719
# Parent  bc264e730103f8b775b2b7c2f202b93a17635e89
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Method.src;

diff -r bc264e730103 -r 80b421d8a8be src/HOL/Import/import_package.ML
--- a/src/HOL/Import/import_package.ML	Wed Apr 13 18:45:38 2005 +0200
+++ b/src/HOL/Import/import_package.ML	Wed Apr 13 18:45:52 2005 +0200
@@ -80,3 +80,4 @@
 
 val setup = [Method.add_method("import",import_meth,"Import HOL4 theorem"),ImportData.init]
 end
+
diff -r bc264e730103 -r 80b421d8a8be src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Apr 13 18:45:38 2005 +0200
+++ b/src/Provers/classical.ML	Wed Apr 13 18:45:52 2005 +0200
@@ -1172,3 +1172,4 @@
 
 
 end;
+