1.1 --- a/src/HOL/ZF/Games.thy	Sun Feb 19 15:40:58 2012 +0100
     1.2 +++ b/src/HOL/ZF/Games.thy	Mon Feb 20 08:01:08 2012 +0100
     1.3 @@ -19,11 +19,7 @@
     1.4    "games_gfp \<equiv> gfp fixgames"
     1.5  
     1.6  lemma mono_fixgames: "mono (fixgames)"
     1.7 -  apply (auto simp add: mono_def fixgames_def)
     1.8 -  apply (rule_tac x=l in exI)
     1.9 -  apply (rule_tac x=r in exI)
    1.10 -  apply auto
    1.11 -  done
    1.12 +  by (auto simp add: mono_def fixgames_def)
    1.13  
    1.14  lemma games_lfp_unfold: "games_lfp = fixgames games_lfp"
    1.15    by (auto simp add: def_lfp_unfold games_lfp_def mono_fixgames)
    1.16 @@ -974,3 +970,4 @@
    1.17  qed
    1.18  
    1.19  end
    1.20 +