--- a/src/FOLP/ex/If.ML Sat Jun 20 20:35:38 1998 +0200
+++ b/src/FOLP/ex/If.ML Mon Jun 22 15:09:59 1998 +0200
@@ -22,7 +22,7 @@
val ifE = result();
-goal If.thy
+Goal
"?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
by (rtac iffI 1);
by (etac ifE 1);
@@ -36,7 +36,7 @@
val if_commute = result();
-goal If.thy "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
+Goal "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
by (fast_tac if_cs 1);
val nested_ifs = result();