# HG changeset patch
# User nipkow
# Date 1415527520 -3600
# Node ID 1694bad185684e161cfdc1a03b3450d8d7ea2df5
# Parent  18750e86d5b873ba114ff651107a24ba7453236e
avoid erule and rotated in IMP

diff -r 18750e86d5b8 -r 1694bad18568 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Sun Nov 09 10:03:18 2014 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Sun Nov 09 11:05:20 2014 +0100
@@ -130,7 +130,7 @@
 
 lemma pfp_inv:
   "pfp f x = Some y \<Longrightarrow> (\<And>x. P x \<Longrightarrow> P(f x)) \<Longrightarrow> P x \<Longrightarrow> P y"
-unfolding pfp_def by (erule while_option_rule [rotated])
+unfolding pfp_def by (blast intro: while_option_rule)
 
 lemma strip_pfp:
 assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0"