src/HOL/BNF/BNF_LFP.thy
changeset 49514 45e3e564e306
parent 49510 ba50d204095e
child 49635 fc0777f04205
--- a/src/HOL/BNF/BNF_LFP.thy	Fri Sep 21 17:41:29 2012 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy	Fri Sep 21 18:25:17 2012 +0200
@@ -145,7 +145,7 @@
 qed
 
 lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r"
-unfolding wo_rel_def card_order_on_def by blast 
+unfolding wo_rel_def card_order_on_def by blast
 
 lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow>
   \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"