src/FOLP/ex/prop.ML

--- a/src/FOLP/ex/prop.ML	Sat Jun 20 20:35:38 1998 +0200
+++ b/src/FOLP/ex/prop.ML	Mon Jun 22 15:09:59 1998 +0200
@@ -11,66 +11,66 @@
 
 
 writeln"commutative laws of & and | ";
-goal thy "?p : P & Q  -->  Q & P";
+Goal "?p : P & Q  -->  Q & P";
 by tac;
 result();
 
-goal thy "?p : P | Q  -->  Q | P";
+Goal "?p : P | Q  -->  Q | P";
 by tac;
 result();
 
 
 writeln"associative laws of & and | ";
-goal thy "?p : (P & Q) & R  -->  P & (Q & R)";
+Goal "?p : (P & Q) & R  -->  P & (Q & R)";
 by tac;
 result();
 
-goal thy "?p : (P | Q) | R  -->  P | (Q | R)";
+Goal "?p : (P | Q) | R  -->  P | (Q | R)";
 by tac;
 result();
 
 
 
 writeln"distributive laws of & and | ";
-goal thy "?p : (P & Q) | R  --> (P | R) & (Q | R)";
+Goal "?p : (P & Q) | R  --> (P | R) & (Q | R)";
 by tac;
 result();
 
-goal thy "?p : (P | R) & (Q | R)  --> (P & Q) | R";
+Goal "?p : (P | R) & (Q | R)  --> (P & Q) | R";
 by tac;
 result();
 
-goal thy "?p : (P | Q) & R  --> (P & R) | (Q & R)";
+Goal "?p : (P | Q) & R  --> (P & R) | (Q & R)";
 by tac;
 result();
 
 
-goal thy "?p : (P & R) | (Q & R)  --> (P | Q) & R";
+Goal "?p : (P & R) | (Q & R)  --> (P | Q) & R";
 by tac;
 result();
 
 
 writeln"Laws involving implication";
 
-goal thy "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)";
+Goal "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)";
 by tac;
 result();
 
 
-goal thy "?p : (P & Q --> R) <-> (P--> (Q-->R))";
+Goal "?p : (P & Q --> R) <-> (P--> (Q-->R))";
 by tac;
 result();
 
 
-goal thy "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R";
+Goal "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R";
 by tac;
 result();
 
-goal thy "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)";
+Goal "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)";
 by tac;
 result();
 
-goal thy "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
+Goal "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
 by tac;
 result();
 
@@ -78,22 +78,22 @@
 writeln"Propositions-as-types";
 
 (*The combinator K*)
-goal thy "?p : P --> (Q --> P)";
+Goal "?p : P --> (Q --> P)";
 by tac;
 result();
 
 (*The combinator S*)
-goal thy "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)";
+Goal "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)";
 by tac;
 result();
 
 
 (*Converse is classical*)
-goal thy "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)";
+Goal "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)";
 by tac;
 result();
 
-goal thy "?p : (P-->Q)  -->  (~Q --> ~P)";
+Goal "?p : (P-->Q)  -->  (~Q --> ~P)";
 by tac;
 result();
 
@@ -101,39 +101,39 @@
 writeln"Schwichtenberg's examples (via T. Nipkow)";
 
 (* stab-imp *)
-goal thy "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q";
+Goal "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q";
 by tac;
 result();
 
 (* stab-to-peirce *)
-goal thy "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
+Goal "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
 \             --> ((P --> Q) --> P) --> P";
 by tac;
 result();
 
 (* peirce-imp1 *)
-goal thy "?p : (((Q --> R) --> Q) --> Q) \
+Goal "?p : (((Q --> R) --> Q) --> Q) \
 \              --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
 by tac;
 result();
   
 (* peirce-imp2 *)
-goal thy "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P";
+Goal "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P";
 by tac;
 result();
 
 (* mints  *)
-goal thy "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q";
+Goal "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q";
 by tac;
 result();
 
 (* mints-solovev *)
-goal thy "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R";
+Goal "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R";
 by tac;
 result();
 
 (* tatsuta *)
-goal thy "?p : (((P7 --> P1) --> P10) --> P4 --> P5) \
+Goal "?p : (((P7 --> P1) --> P10) --> P4 --> P5) \
 \         --> (((P8 --> P2) --> P9) --> P3 --> P10) \
 \         --> (P1 --> P8) --> P6 --> P7 \
 \         --> (((P3 --> P2) --> P9) --> P4) \
@@ -142,7 +142,7 @@
 result();
 
 (* tatsuta1 *)
-goal thy "?p : (((P8 --> P2) --> P9) --> P3 --> P10) \
+Goal "?p : (((P8 --> P2) --> P9) --> P3 --> P10) \
 \    --> (((P3 --> P2) --> P9) --> P4) \
 \    --> (((P6 --> P1) --> P2) --> P9) \
 \    --> (((P7 --> P1) --> P10) --> P4 --> P5) \