equal
deleted
inserted
replaced
50 lemma "\<exists>x (y\<Colon>bool one_or_two). x \<noteq> y" |
50 lemma "\<exists>x (y\<Colon>bool one_or_two). x \<noteq> y" |
51 nitpick [card = 1, expect = potential] (* unfortunate *) |
51 nitpick [card = 1, expect = potential] (* unfortunate *) |
52 nitpick [card = 2, expect = none] |
52 nitpick [card = 2, expect = none] |
53 oops |
53 oops |
54 |
54 |
55 definition "bounded = {n\<Colon>nat. finite (UNIV\<Colon>'a \<Rightarrow> bool) \<longrightarrow> n < card (UNIV\<Colon>'a \<Rightarrow> bool)}" |
55 definition "bounded = {n\<Colon>nat. finite (UNIV \<Colon> 'a set) \<longrightarrow> n < card (UNIV \<Colon> 'a set)}" |
|
56 |
56 typedef (open) 'a bounded = "bounded(TYPE('a))" |
57 typedef (open) 'a bounded = "bounded(TYPE('a))" |
57 unfolding bounded_def |
58 unfolding bounded_def |
58 apply (rule_tac x = 0 in exI) |
59 apply (rule_tac x = 0 in exI) |
59 apply (case_tac "card UNIV = 0") |
60 apply (case_tac "card UNIV = 0") |
60 by auto |
61 by auto |