# HG changeset patch
# User blanchet
# Date 1409652553 -7200
# Node ID 10f92532f128b0e01d765613d564a00232cfb24c
# Parent  b563ec62d04e18ae5d1d2959ddb86bfd6de711eb
tuning

diff -r b563ec62d04e -r 10f92532f128 src/HOL/BNF_Least_Fixpoint.thy
--- a/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 02 08:24:42 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 02 12:09:13 2014 +0200
@@ -155,16 +155,12 @@
 lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
 by auto
 
-(*helps resolution*)
-lemma well_order_induct_imp:
-  "wo_rel r \<Longrightarrow> (\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> y \<in> Field r \<longrightarrow> P y \<Longrightarrow> x \<in> Field r \<longrightarrow> P x) \<Longrightarrow>
-     x \<in> Field r \<longrightarrow> P x"
-by (erule wo_rel.well_order_induct)
+lemmas well_order_induct_imp = wo_rel.well_order_induct[of r "\<lambda>x. x \<in> Field r \<longrightarrow> P x" for r P]
 
 lemma meta_spec2:
   assumes "(\<And>x y. PROP P x y)"
   shows "PROP P x y"
-by (rule assms)
+  by (rule assms)
 
 lemma nchotomy_relcomppE:
   assumes "\<And>y. \<exists>x. y = f x" "(r OO s) a c" "\<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P"