| changeset 62390 | 842917225d56 |
| parent 62131 | 1baed43f453e |
| child 63092 | a949b2a5f51d |
--- a/src/HOL/Library/Nonpos_Ints.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Library/Nonpos_Ints.thy Tue Feb 23 16:25:08 2016 +0100 @@ -301,4 +301,4 @@ lemma ii_not_nonpos_Reals [iff]: "\<i> \<notin> \<real>\<^sub>\<le>\<^sub>0" by (simp add: complex_nonpos_Reals_iff) -end \ No newline at end of file +end