src/FOLP/ex/prop.ML
changeset 17480 fd19f77dcf60
parent 5061 f947332d5465
child 25991 31b38a39e589
     1.1 --- a/src/FOLP/ex/prop.ML	Sat Sep 17 20:49:14 2005 +0200
     1.2 +++ b/src/FOLP/ex/prop.ML	Sun Sep 18 14:25:48 2005 +0200
     1.3 @@ -7,9 +7,6 @@
     1.4  Needs declarations of the theory "thy" and the tactic "tac"
     1.5  *)
     1.6  
     1.7 -writeln"File FOLP/ex/prop.ML";
     1.8 -
     1.9 -
    1.10  writeln"commutative laws of & and | ";
    1.11  Goal "?p : P & Q  -->  Q & P";
    1.12  by tac;
    1.13 @@ -149,5 +146,3 @@
    1.14  \    --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5";
    1.15  by tac;
    1.16  result();
    1.17 -
    1.18 -writeln"Reached end of file.";