--- 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);