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