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.
tuned;
authorwenzelm
Tue, 05 Jan 2016 15:35:08 +0100
changeset 62061 bd2ccef8209b
parent 62059 2da6f4945295
child 62062 ee610059b0e9
tuned;
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle