# HG changeset patch
# User paulson
# Date 932563398 -7200
# Node ID 8dfea70eb6b7fe845f537f0e126d51135db511a3
# Parent  b9ddbb92593909f8bc9ffaadd3116a1b06ab30ed
removed 2 qed_goals

diff -r b9ddbb925939 -r 8dfea70eb6b7 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed Jul 21 15:22:11 1999 +0200
+++ b/src/HOL/Nat.ML	Wed Jul 21 15:23:18 1999 +0200
@@ -60,49 +60,49 @@
 by Auto_tac;
 qed "less_Suc_eq_0_disj";
 
-qed_goalw "Least_Suc" thy [Least_nat_def]
- "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
- (fn _ => [
-        rtac select_equality 1,
-        fold_goals_tac [Least_nat_def],
-        safe_tac (claset() addSEs [LeastI]),
-        rename_tac "j" 1,
-        exhaust_tac "j" 1,
-        Blast_tac 1,
-        blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1,
-        rename_tac "k n" 1,
-        exhaust_tac "k" 1,
-        Blast_tac 1,
-        hyp_subst_tac 1,
-        rewtac Least_nat_def,
-        rtac (select_equality RS arg_cong RS sym) 1,
-        Safe_tac,
-        dtac Suc_mono 1,
-        Blast_tac 1,
-        cut_facts_tac [less_linear] 1,
-        Safe_tac,
-        atac 2,
-        Blast_tac 2,
-        dtac Suc_mono 1,
-        Blast_tac 1]);
+Goalw [Least_nat_def]
+ "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
+by (rtac select_equality 1);
+by (fold_goals_tac [Least_nat_def]);
+by (safe_tac (claset() addSEs [LeastI]));
+by (rename_tac "j" 1);
+by (exhaust_tac "j" 1);
+by (Blast_tac 1);
+by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
+by (rename_tac "k n" 1);
+by (exhaust_tac "k" 1);
+by (Blast_tac 1);
+by (hyp_subst_tac 1);
+by (rewtac Least_nat_def);
+by (rtac (select_equality RS arg_cong RS sym) 1);
+by (Safe_tac);
+by (dtac Suc_mono 1);
+by (Blast_tac 1);
+by (cut_facts_tac [less_linear] 1);
+by (Safe_tac);
+by (atac 2);
+by (Blast_tac 2);
+by (dtac Suc_mono 1);
+by (Blast_tac 1);
+qed "Least_Suc";
 
-qed_goal "nat_induct2" thy 
-"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [
-        cut_facts_tac prems 1,
-        rtac less_induct 1,
-        exhaust_tac "n" 1,
-         hyp_subst_tac 1,
-         atac 1,
-        hyp_subst_tac 1,
-        exhaust_tac "nat" 1,
-         hyp_subst_tac 1,
-         atac 1,
-        hyp_subst_tac 1,
-        resolve_tac prems 1,
-        dtac spec 1,
-        etac mp 1,
-        rtac (lessI RS less_trans) 1,
-        rtac (lessI RS Suc_mono) 1]);
+val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
+by (cut_facts_tac prems 1);
+by (rtac less_induct 1);
+by (exhaust_tac "n" 1);
+by (hyp_subst_tac 1);
+by (atac 1);
+by (hyp_subst_tac 1);
+by (exhaust_tac "nat" 1);
+by (hyp_subst_tac 1);
+by (atac 1);
+by (hyp_subst_tac 1);
+by (resolve_tac prems 1);
+by (dtac spec 1);
+by (etac mp 1);
+by (rtac (lessI RS less_trans) 1);
+by (rtac (lessI RS Suc_mono) 1);
+qed "nat_induct2";
 
 Goal "min 0 n = 0";
 by (rtac min_leastL 1);