--- 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
+