# HG changeset patch
# User haftmann
# Date 1329721268 -3600
# Node ID c2b5900988e2792db1f8a820d137a5b7e5afde60
# Parent  87d4e49584769c9c08a02b3b6f0ad938d39fded0
tuned proof

diff -r 87d4e4958476 -r c2b5900988e2 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Sun Feb 19 15:40:58 2012 +0100
+++ b/src/HOL/ZF/Games.thy	Mon Feb 20 08:01:08 2012 +0100
@@ -19,11 +19,7 @@
   "games_gfp \<equiv> gfp fixgames"
 
 lemma mono_fixgames: "mono (fixgames)"
-  apply (auto simp add: mono_def fixgames_def)
-  apply (rule_tac x=l in exI)
-  apply (rule_tac x=r in exI)
-  apply auto
-  done
+  by (auto simp add: mono_def fixgames_def)
 
 lemma games_lfp_unfold: "games_lfp = fixgames games_lfp"
   by (auto simp add: def_lfp_unfold games_lfp_def mono_fixgames)
@@ -974,3 +970,4 @@
 qed
 
 end
+