--- a/src/FOLP/ex/If.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/ex/If.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOLP/ex/if
+(* Title: FOLP/ex/if
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
For ex/if.thy. First-Order Logic: the 'if' example
@@ -24,11 +24,11 @@
goal If.thy
"?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
-by (resolve_tac [iffI] 1);
-by (eresolve_tac [ifE] 1);
-by (eresolve_tac [ifE] 1);
-by (resolve_tac [ifI] 1);
-by (resolve_tac [ifI] 1);
+by (rtac iffI 1);
+by (etac ifE 1);
+by (etac ifE 1);
+by (rtac ifI 1);
+by (rtac ifI 1);
choplev 0;
val if_cs = FOLP_cs addSIs [ifI] addSEs[ifE];