src/HOL/ex/set.thy
changeset 14353 79f9fbef9106
parent 13107 8743cc847224
child 15306 51f3d31e8eea
equal deleted inserted replaced
14352:a8b1a44d8264 14353:79f9fbef9106
   154   -- {* Example 7. *}
   154   -- {* Example 7. *}
   155   by force
   155   by force
   156 
   156 
   157 lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
   157 lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
   158     \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
   158     \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
   159   -- {* Example 8. *}
   159   -- {* Example 8 now needs a small hint. *}
   160   by force  -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
   160   by (simp add: abs_if, force)
       
   161     -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
   161 
   162 
   162 text {* Example 9 omitted (requires the reals). *}
   163 text {* Example 9 omitted (requires the reals). *}
   163 
   164 
   164 text {* The paper has no Example 10! *}
   165 text {* The paper has no Example 10! *}
   165 
   166