# HG changeset patch
# User wenzelm
# Date 1006904228 -3600
# Node ID 67ca723a02ddc8d2b034a6c73fb324182f1d5c97
# Parent  87d1bddcdfe73c4a7b04a79983cf33ba0e32eb04
tuned;

diff -r 87d1bddcdfe7 -r 67ca723a02dd src/FOL/FOL.ML
--- a/src/FOL/FOL.ML	Tue Nov 27 13:28:26 2001 +0100
+++ b/src/FOL/FOL.ML	Wed Nov 28 00:37:08 2001 +0100
@@ -5,6 +5,4 @@
   val classical = classical;
 end;
 
-AddXEs [disjI1, disjI2];
-
 open FOL;
diff -r 87d1bddcdfe7 -r 67ca723a02dd src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Tue Nov 27 13:28:26 2001 +0100
+++ b/src/FOL/FOL.thy	Wed Nov 28 00:37:08 2001 +0100
@@ -26,6 +26,8 @@
 setup Cla.setup
 setup clasetup
 
+declare disjI1 [elim?]  disjI2 [elim?]
+
 use "blastdata.ML"
 setup Blast.setup
 use "FOL_lemmas2.ML"