src/HOLCF/Tr.ML

--- a/src/HOLCF/Tr.ML	Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/Tr.ML	Tue Dec 16 17:58:03 1997 +0100
@@ -115,17 +115,17 @@
 "!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)";
 by (rtac iffI 1);
 by (res_inst_tac [("p","t")] trE 1);
-auto();
+by (Auto_tac());
 by (res_inst_tac [("p","t")] trE 1);
-auto();
+by (Auto_tac());
 qed"andalso_or";
 
 goal thy "!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
 by (rtac iffI 1);
 by (res_inst_tac [("p","t")] trE 1);
-auto();
+by (Auto_tac());
 by (res_inst_tac [("p","t")] trE 1);
-auto();
+by (Auto_tac());
 qed"andalso_and";
 
 goal thy "(Def x ~=FF)= x";