changeset 56544 | b60d5d119489 |
parent 54863 | 82acc20ded73 |
child 57492 | 74bf65a1910a |
--- a/src/HOL/ex/Dedekind_Real.thy Fri Apr 11 23:22:00 2014 +0200 +++ b/src/HOL/ex/Dedekind_Real.thy Sat Apr 12 17:26:27 2014 +0200 @@ -368,7 +368,7 @@ from preal_exists_bound [OF B] obtain y where 2 [simp]: "0 < y" "y \<notin> B" by blast show ?thesis proof (intro exI conjI) - show "0 < x*y" by (simp add: mult_pos_pos) + show "0 < x*y" by simp show "x * y \<notin> mult_set A B" proof - {