src/HOL/ex/Primrec.thy
changeset 16563 a92f96951355
parent 16417 9bc16273c2d4
child 16588 8de758143786
     1.1 --- a/src/HOL/ex/Primrec.thy	Fri Jun 24 16:21:01 2005 +0200
     1.2 +++ b/src/HOL/ex/Primrec.thy	Fri Jun 24 17:25:10 2005 +0200
     1.3 @@ -286,12 +286,8 @@
     1.4    ==> \<exists>k. \<forall>l. COMP g fs  l < ack(k, list_add l)"
     1.5    apply (unfold COMP_def)
     1.6    apply (frule Int_lower1 [THEN lists_mono, THEN subsetD])
     1.7 -  apply (erule COMP_map_aux [THEN exE])
     1.8 -  apply (rule exI)
     1.9 -  apply (rule allI)
    1.10 -  apply (drule spec)+
    1.11 -  apply (erule less_trans)
    1.12 -  apply (blast intro: ack_less_mono2 ack_nest_bound less_trans)
    1.13 +  apply (drule COMP_map_aux)
    1.14 +  apply (meson ack_less_mono2 ack_nest_bound less_trans)
    1.15    done
    1.16  
    1.17