# HG changeset patch
# User nipkow
# Date 1508666384 -7200
# Node ID c08d7349774eaae0a9b70066b4cb5dedda8969e6
# Parent  ced164fe3bbd12b27d53e7230a27faa7f5196bba
tuned

diff -r ced164fe3bbd -r c08d7349774e src/HOL/ZF/Games.thy
--- 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