Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid slow metis proof;
authorwenzelm
Sat, 08 Nov 2014 16:42:04 +0100
changeset 58947 79684150ed6a
parent 58946 3bf80312508e
child 58948 f6ecc0fb2066
avoid slow metis proof;
src/HOL/IMP/Abs_Int0.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/IMP/Abs_Int0.thy	Sat Nov 08 16:35:24 2014 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Sat Nov 08 16:42:04 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 (metis (lifting) while_option_rule)
+unfolding pfp_def by (erule while_option_rule [rotated])
 
 lemma strip_pfp:
 assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0"
isabelle