| changeset 31100 | 6a2e67fe4488 |
| parent 31024 | 0fdf666e08bf |
| child 31155 | 92d8ff6af82c |
--- a/src/HOL/Nat.thy Mon May 11 11:53:21 2009 +0200 +++ b/src/HOL/Nat.thy Mon May 11 15:18:32 2009 +0200 @@ -1410,6 +1410,7 @@ declaration {* K Nat_Arith.setup *} use "Tools/lin_arith.ML" +setup {* Lin_Arith.global_setup *} declaration {* K Lin_Arith.setup *} lemmas [arith_split] = nat_diff_split split_min split_max