| changeset 31082 | 54a442b2d727 |
| parent 30235 | 58d147683393 |
| child 32436 | 10cd49e0c067 |
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri May 08 13:38:21 2009 +0200 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Sat May 09 09:17:29 2009 +0200 @@ -454,7 +454,7 @@ apply (simp add: max_of_list_def) apply (induct xs) apply simp -using [[fast_arith_split_limit = 0]] +using [[linarith_split_limit = 0]] apply simp apply arith done