Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Nonpos_Ints.thy
changeset 63092 a949b2a5f51d
parent 62390 842917225d56
child 67135 1a94352812f4 
--- a/src/HOL/Library/Nonpos_Ints.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Nonpos_Ints.thy	Fri May 13 20:24:10 2016 +0200
@@ -54,7 +54,7 @@
 
 lemma nonpos_IntsI: 
   "x \<in> \<int> \<Longrightarrow> x \<le> 0 \<Longrightarrow> (x :: 'a :: linordered_idom) \<in> \<int>\<^sub>\<le>\<^sub>0"
-  using assms unfolding nonpos_Ints_def Ints_def by auto
+  unfolding nonpos_Ints_def Ints_def by auto
 
 lemma nonpos_Ints_subset_Ints: "\<int>\<^sub>\<le>\<^sub>0 \<subseteq> \<int>"
   unfolding nonpos_Ints_def Ints_def by blast
isabelle