# HG changeset patch
# User wenzelm
# Date 1007517589 -3600
# Node ID 1cee8a0db39238c30eee04a8f7b24b5024e355e2
# Parent  f0fd3c4f2f492ced774c5929605bc2cc6b0aeb22
removed declaration of disjI1, disjI2 (already done in IFOL);

diff -r f0fd3c4f2f49 -r 1cee8a0db392 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Wed Dec 05 02:59:15 2001 +0100
+++ b/src/FOL/FOL.thy	Wed Dec 05 02:59:49 2001 +0100
@@ -26,8 +26,6 @@
 setup Cla.setup
 setup clasetup
 
-declare disjI1 [elim?]  disjI2 [elim?]
-
 use "blastdata.ML"
 setup Blast.setup
 use "FOL_lemmas2.ML"