--- a/src/FOLP/ex/Prolog.ML Tue Jan 30 15:12:53 1996 +0100
+++ b/src/FOLP/ex/Prolog.ML Tue Jan 30 15:19:20 1996 +0100
@@ -1,4 +1,4 @@
-(* Title: FOL/ex/prolog.ML
+(* Title: FOLP/ex/prolog.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
--- a/src/FOLP/ex/ROOT.ML Tue Jan 30 15:12:53 1996 +0100
+++ b/src/FOLP/ex/ROOT.ML Tue Jan 30 15:19:20 1996 +0100
@@ -22,7 +22,6 @@
val thy = IFOLP.thy and tac = Int.fast_tac 1;
time_use "prop.ML";
time_use "quant.ML";
-commit();
writeln"\n** Classical examples **\n";
time_use "cla.ML";
--- a/src/FOLP/ex/cla.ML Tue Jan 30 15:12:53 1996 +0100
+++ b/src/FOLP/ex/cla.ML Tue Jan 30 15:19:20 1996 +0100
@@ -6,7 +6,7 @@
Classical First-Order Logic
*)
-writeln"File FOL/ex/cla.";
+writeln"File FOLP/ex/cla.ML";
open Cla; (*in case structure Int is open!*)
--- a/src/FOLP/ex/foundn.ML Tue Jan 30 15:12:53 1996 +0100
+++ b/src/FOLP/ex/foundn.ML Tue Jan 30 15:19:20 1996 +0100
@@ -1,4 +1,4 @@
-(* Title: FOL/ex/foundn
+(* Title: FOLP/ex/foundn.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -6,7 +6,7 @@
Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
*)
-writeln"File FOL/ex/foundn.";
+writeln"File FOLP/ex/foundn.ML";
goal IFOLP.thy "?p : A&B --> (C-->A&C)";
by (rtac impI 1);
--- a/src/FOLP/ex/int.ML Tue Jan 30 15:12:53 1996 +0100
+++ b/src/FOLP/ex/int.ML Tue Jan 30 15:19:20 1996 +0100
@@ -1,4 +1,4 @@
-(* Title: FOL/ex/int
+(* Title: FOLP/ex/int.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -15,7 +15,7 @@
by (Int.fast_tac 1);
*)
-writeln"File FOL/ex/int.";
+writeln"File FOLP/ex/int.ML";
(*Note: for PROPOSITIONAL formulae...
~A is classically provable iff it is intuitionistically provable.
--- a/src/FOLP/ex/intro.ML Tue Jan 30 15:12:53 1996 +0100
+++ b/src/FOLP/ex/intro.ML Tue Jan 30 15:19:20 1996 +0100
@@ -1,4 +1,4 @@
-(* Title: FOL/ex/intro
+(* Title: FOLP/ex/intro.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
--- a/src/FOLP/ex/prop.ML Tue Jan 30 15:12:53 1996 +0100
+++ b/src/FOLP/ex/prop.ML Tue Jan 30 15:19:20 1996 +0100
@@ -1,4 +1,4 @@
-(* Title: FOL/ex/prop
+(* Title: FOLP/ex/prop.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -7,7 +7,7 @@
Needs declarations of the theory "thy" and the tactic "tac"
*)
-writeln"File FOL/ex/prop.";
+writeln"File FOLP/ex/prop.ML";
writeln"commutative laws of & and | ";
--- a/src/FOLP/ex/quant.ML Tue Jan 30 15:12:53 1996 +0100
+++ b/src/FOLP/ex/quant.ML Tue Jan 30 15:19:20 1996 +0100
@@ -1,4 +1,4 @@
-(* Title: FOL/ex/quant
+(* Title: FOLP/ex/quant.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -7,7 +7,7 @@
Needs declarations of the theory "thy" and the tactic "tac"
*)
-writeln"File FOL/ex/quant.";
+writeln"File FOLP/ex/quant.ML";
goal thy "?p : (ALL x y.P(x,y)) --> (ALL y x.P(x,y))";
by tac;