changeset 9969 | 4753185f1dd2 |
parent 9870 | 2374ba026fc6 |
child 10186 | 499637e8f2c6 |
--- a/src/HOL/NatDef.ML Fri Sep 15 11:34:46 2000 +0200 +++ b/src/HOL/NatDef.ML Fri Sep 15 12:39:57 2000 +0200 @@ -476,7 +476,7 @@ val [prem1,prem2] = Goalw [Least_nat_def] "[| P(k::nat); !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k"; -by (rtac select_equality 1); +by (rtac some_equality 1); by (blast_tac (claset() addSIs [prem1,prem2]) 1); by (cut_facts_tac [less_linear] 1); by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1);