1855 Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def, |
1855 Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def, |
1856 real_of_posnat_def,hypreal_one_def,real_of_nat_def] |
1856 real_of_posnat_def,hypreal_one_def,real_of_nat_def] |
1858 by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1); |
1858 by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1); |