| changeset 24110 | 4ab3084e311c |
| parent 24078 | 04b28c723d43 |
| child 30235 | 58d147683393 |
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Aug 01 16:50:16 2007 +0200 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Aug 01 16:55:37 2007 +0200 @@ -454,7 +454,7 @@ apply (simp add: max_of_list_def) apply (induct xs) apply simp -using [[option fast_arith_split_limit = 0]] +using [[fast_arith_split_limit = 0]] apply simp apply arith done