# HG changeset patch
# User wenzelm
# Date 1135207754 -3600
# Node ID b75ce99617c75ac648d3bc0a86fe1979cdf7f867
# Parent  8ac97f71369d58fd7efe363598d02ea6281b081c
structure ProjectRule;

diff -r 8ac97f71369d -r b75ce99617c7 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Thu Dec 22 00:29:12 2005 +0100
+++ b/src/FOL/IFOL.thy	Thu Dec 22 00:29:14 2005 +0100
@@ -143,6 +143,15 @@
 
 use "IFOL_lemmas.ML"
 
+ML {*
+structure ProjectRule = ProjectRuleFun
+(struct
+  val conjunct1 = thm "conjunct1";
+  val conjunct2 = thm "conjunct2";
+  val mp = thm "mp";
+end)
+*}
+
 use "fologic.ML"
 use "hypsubstdata.ML"
 setup hypsubst_setup