src/FOLP/ex/prop.ML

--- a/src/FOLP/ex/prop.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/prop.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -7,9 +7,6 @@
 Needs declarations of the theory "thy" and the tactic "tac"
 *)
 
-writeln"File FOLP/ex/prop.ML";
-
-
 writeln"commutative laws of & and | ";
 Goal "?p : P & Q  -->  Q & P";
 by tac;
@@ -149,5 +146,3 @@
 \    --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5";
 by tac;
 result();
-
-writeln"Reached end of file.";