src/HOL/ex/set.thy
 changeset 14353 79f9fbef9106 parent 13107 8743cc847224 child 15306 51f3d31e8eea
equal 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 `