equal
deleted
inserted
replaced
127 add_numeral_special |
127 add_numeral_special |
128 add_neg_numeral_special |
128 add_neg_numeral_special |
129 mult_1_left |
129 mult_1_left |
130 mult_1_right |
130 mult_1_right |
131 |
131 |
132 ML_file "normarith.ML" |
132 ML_file \<open>normarith.ML\<close> |
133 |
133 |
134 method_setup%important norm = \<open> |
134 method_setup%important norm = \<open> |
135 Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) |
135 Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) |
136 \<close> "prove simple linear statements about vector norms" |
136 \<close> "prove simple linear statements about vector norms" |
137 |
137 |