src/FOLP/ex/prop.ML
changeset 1464 a608f83e3421
parent 1459 d12da312eff4
child 5061 f947332d5465
--- 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 | ";