--- a/src/FOLP/IFOLP.thy Mon Oct 20 11:01:07 1997 +0200
+++ b/src/FOLP/IFOLP.thy Mon Oct 20 11:06:01 1997 +0200
@@ -8,6 +8,8 @@
IFOLP = Pure +
+global
+
classes term < logic
default term
@@ -59,6 +61,8 @@
idpeel :: "[p,'a=>p]=>p"
nrm, NRM :: "p"
+local
+
rules
(**** Propositional logic ****)