--- 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;