--- a/src/FOL/IFOL.ML Sun Nov 26 23:09:25 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-
-structure IFOL =
-struct
- val thy = the_context ();
- val refl = refl;
- val subst = subst;
- val conjI = conjI;
- val conjunct1 = conjunct1;
- val conjunct2 = conjunct2;
- val disjI1 = disjI1;
- val disjI2 = disjI2;
- val disjE = disjE;
- val impI = impI;
- val mp = mp;
- val FalseE = FalseE;
- val True_def = True_def;
- val not_def = not_def;
- val iff_def = iff_def;
- val ex1_def = ex1_def;
- val allI = allI;
- val spec = spec;
- val exI = exI;
- val exE = exE;
- val eq_reflection = eq_reflection;
- val iff_reflection = iff_reflection;
-end;