src/HOL/ex/set.thy
changeset 34055 fdf294ee08b2
parent 33057 764547b68538
child 36319 8feb2c4bef1a
     1.1 --- a/src/HOL/ex/set.thy	Thu Dec 10 17:34:09 2009 +0000
     1.2 +++ b/src/HOL/ex/set.thy	Thu Dec 10 17:34:18 2009 +0000
     1.3 @@ -205,10 +205,7 @@
     1.4  lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
     1.5    P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
     1.6    -- {* Example 11: needs a hint. *}
     1.7 -  apply clarify
     1.8 -  apply (drule_tac x = "{x. P x}" in spec)
     1.9 -  apply force
    1.10 -  done
    1.11 +by(metis Nat.induct)
    1.12  
    1.13  lemma
    1.14    "(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
    1.15 @@ -223,8 +220,7 @@
    1.16        to require arithmetic reasoning. *}
    1.17    apply clarify
    1.18    apply (rule_tac x = "{x. \<exists>u. x = 2 * u}" in exI, auto)
    1.19 -   apply (case_tac v, auto)
    1.20 -  apply (drule_tac x = "Suc v" and P = "\<lambda>x. ?a x \<noteq> ?b x" in spec, force)
    1.21 +   apply metis+
    1.22    done
    1.23  
    1.24  end