--- a/src/FOL/ex/Nat.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/Nat.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/nat.ML
+(* Title: FOL/ex/nat.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Examples for the manual "Introduction to Isabelle"
@@ -17,17 +17,17 @@
goal Nat.thy "Suc(k) ~= k";
by (res_inst_tac [("n","k")] induct 1);
-by (resolve_tac [notI] 1);
-by (eresolve_tac [Suc_neq_0] 1);
-by (resolve_tac [notI] 1);
-by (eresolve_tac [notE] 1);
-by (eresolve_tac [Suc_inject] 1);
+by (rtac notI 1);
+by (etac Suc_neq_0 1);
+by (rtac notI 1);
+by (etac notE 1);
+by (etac Suc_inject 1);
qed "Suc_n_not_n";
goal Nat.thy "(k+m)+n = k+(m+n)";
prths ([induct] RL [topthm()]); (*prints all 14 next states!*)
-by (resolve_tac [induct] 1);
+by (rtac induct 1);
back();
back();
back();
@@ -36,11 +36,11 @@
back();
goalw Nat.thy [add_def] "0+n = n";
-by (resolve_tac [rec_0] 1);
+by (rtac rec_0 1);
qed "add_0";
goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
-by (resolve_tac [rec_Suc] 1);
+by (rtac rec_Suc 1);
qed "add_Suc";
val add_ss = FOL_ss addsimps [add_0, add_Suc];