src/FOL/ex/int.ML

 goal IFOL.thy "(P&Q) <-> P <-> Q <-> (P|Q)";
 by (Int.fast_tac 1);
 result();
 
 
-writeln"U****Examples with quantifiers****";
+writeln"****Examples with quantifiers****";
 
 
 writeln"The converse is classical in the following implications...";
 
 goal IFOL.thy "(EX x.P(x)-->Q)  -->  (ALL x.P(x)) --> Q";