# HG changeset patch
# User clasohm
# Date 823011560 -3600
# Node ID a608f83e3421f447d0f2a3c6427200211cb2dcdf
# Parent  49ca5e8756912f2fc59a292b21484e139f0e2665
expanded tabs; removed commit() from ROOT.ML

diff -r 49ca5e875691 -r a608f83e3421 src/FOLP/ex/Prolog.ML
--- 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
diff -r 49ca5e875691 -r a608f83e3421 src/FOLP/ex/ROOT.ML
--- 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";
diff -r 49ca5e875691 -r a608f83e3421 src/FOLP/ex/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!*)
 
diff -r 49ca5e875691 -r a608f83e3421 src/FOLP/ex/foundn.ML
--- 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);
diff -r 49ca5e875691 -r a608f83e3421 src/FOLP/ex/int.ML
--- 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.  
diff -r 49ca5e875691 -r a608f83e3421 src/FOLP/ex/intro.ML
--- 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
diff -r 49ca5e875691 -r a608f83e3421 src/FOLP/ex/prop.ML
--- 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 | ";
diff -r 49ca5e875691 -r a608f83e3421 src/FOLP/ex/quant.ML
--- 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;