equal
deleted
inserted
replaced
59 by (auto, case_tac x, auto) |
59 by (auto, case_tac x, auto) |
60 finally show "finite (UNIV :: 'a discr set)" . |
60 finally show "finite (UNIV :: 'a discr set)" . |
61 qed |
61 qed |
62 |
62 |
63 instance discr :: (type) chfin |
63 instance discr :: (type) chfin |
64 apply (intro_classes, clarify) |
64 apply intro_classes |
65 apply (rule_tac x=0 in exI) |
65 apply (rule_tac x=0 in exI) |
66 apply (unfold max_in_chain_def) |
66 apply (unfold max_in_chain_def) |
67 apply (clarify, erule discr_chain0 [symmetric]) |
67 apply (clarify, erule discr_chain0 [symmetric]) |
68 done |
68 done |
69 |
69 |