changeset 69605 | a96320074298 |
parent 69565 | 1daf07b65385 |
child 70136 | f03a01a18c6e |
--- a/src/HOL/Analysis/Norm_Arith.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Analysis/Norm_Arith.thy Sun Jan 06 15:04:34 2019 +0100 @@ -129,7 +129,7 @@ mult_1_left mult_1_right -ML_file "normarith.ML" +ML_file \<open>normarith.ML\<close> method_setup%important norm = \<open> Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)