| changeset 11701 | 3d51fbf81c17 |
| parent 11655 | 923e4d0d36d5 |
| child 11713 | 883d559b0b8c |
--- a/src/HOL/Real/RealDef.ML Fri Oct 05 21:50:37 2001 +0200 +++ b/src/HOL/Real/RealDef.ML Fri Oct 05 21:52:39 2001 +0200 @@ -130,7 +130,7 @@ by (asm_full_simp_tac (simpset() addsimps [real_minus_minus]) 1); qed "inj_real_minus"; -Goalw [real_zero_def] "-0 = (0::real)"; +Goalw [real_zero_def] "- 0 = (0::real)"; by (simp_tac (simpset() addsimps [real_minus]) 1); qed "real_minus_zero";