equal
deleted
inserted
replaced
791 |
791 |
792 instance |
792 instance |
793 apply (intro_classes, unfold real_norm_def real_scaleR_def) |
793 apply (intro_classes, unfold real_norm_def real_scaleR_def) |
794 apply (rule dist_real_def) |
794 apply (rule dist_real_def) |
795 apply (rule open_real_def) |
795 apply (rule open_real_def) |
796 apply (simp add: real_sgn_def) |
796 apply (simp add: sgn_real_def) |
797 apply (rule abs_ge_zero) |
797 apply (rule abs_ge_zero) |
798 apply (rule abs_eq_0) |
798 apply (rule abs_eq_0) |
799 apply (rule abs_triangle_ineq) |
799 apply (rule abs_triangle_ineq) |
800 apply (rule abs_mult) |
800 apply (rule abs_mult) |
801 apply (rule abs_mult) |
801 apply (rule abs_mult) |