changeset 62061 | bd2ccef8209b |
parent 61945 | 1135b8de26c3 |
child 62381 | a6479cb85944 |
child 62390 | 842917225d56 |
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Jan 05 14:25:12 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Jan 05 15:35:08 2016 +0100 @@ -52,7 +52,7 @@ lemma swap_apply2: "Fun.swap x y f y = f x" by (simp add: Fun.swap_def) -lemma (in -) lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0" +lemma lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0" by auto lemma Zero_notin_Suc: "0 \<notin> Suc ` A"