| changeset 25921 | 0ca392ab7f37 |
| parent 25906 | 2179c6661218 |
| child 26025 | ca6876116bb4 |
--- a/src/HOLCF/Discrete.thy Wed Jan 16 22:41:49 2008 +0100 +++ b/src/HOLCF/Discrete.thy Thu Jan 17 00:51:20 2008 +0100 @@ -61,7 +61,7 @@ qed instance discr :: (type) chfin -apply (intro_classes, clarify) +apply intro_classes apply (rule_tac x=0 in exI) apply (unfold max_in_chain_def) apply (clarify, erule discr_chain0 [symmetric])