--- a/src/FOLP/FOLP.ML Thu Jun 01 13:25:06 1995 +0200
+++ b/src/FOLP/FOLP.ML Fri Jun 02 10:38:48 1995 +0200
@@ -1,9 +1,9 @@
-(* Title: FOL/fol.ML
+(* Title: FOLP/FOLP.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-Tactics and lemmas for fol.thy (classical First-Order Logic)
+Tactics and lemmas for FOLP (Classical First-Order Logic with Proofs)
*)
open FOLP;
--- a/src/FOLP/FOLP.thy Thu Jun 01 13:25:06 1995 +0200
+++ b/src/FOLP/FOLP.thy Fri Jun 02 10:38:48 1995 +0200
@@ -1,3 +1,11 @@
+(* Title: FOLP/FOLP.thy
+ ID: $Id$
+ Author: Martin D Coen, Cambridge University Computer Laboratory
+ Copyright 1992 University of Cambridge
+
+Classical First-Order Logic with Proofs
+*)
+
FOLP = IFOLP +
consts
cla :: "[p=>p]=>p"
--- a/src/FOLP/IFOLP.ML Thu Jun 01 13:25:06 1995 +0200
+++ b/src/FOLP/IFOLP.ML Fri Jun 02 10:38:48 1995 +0200
@@ -1,9 +1,9 @@
-(* Title: FOLP/ifol.ML
+(* Title: FOLP/IFOLP.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Tactics and lemmas for ifol.thy (intuitionistic first-order logic)
+Tactics and lemmas for IFOLP (Intuitionistic First-Order Logic with Proofs)
*)
open IFOLP;
--- a/src/FOLP/IFOLP.thy Thu Jun 01 13:25:06 1995 +0200
+++ b/src/FOLP/IFOLP.thy Fri Jun 02 10:38:48 1995 +0200
@@ -1,3 +1,11 @@
+(* Title: FOLP/IFOLP.thy
+ ID: $Id$
+ Author: Martin D Coen, Cambridge University Computer Laboratory
+ Copyright 1992 University of Cambridge
+
+Intuitionistic First-Order Logic with Proofs
+*)
+
IFOLP = Pure +
classes term < logic