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