--- a/src/HOL/ZF/Games.thy Sun Oct 22 09:10:10 2017 +0200
+++ b/src/HOL/ZF/Games.thy Sun Oct 22 11:59:44 2017 +0200
@@ -153,7 +153,7 @@
}
note games = this
show ?thesis
- apply (rule iff[rule_format])
+ apply (rule iffI)
apply (erule games)
apply (simp add: games_lfp_unfold[symmetric])
done