src/HOL/Integ/IntDiv_setup.ML
changeset 17609 5156b731ebc8
parent 14479 0eca4aabf371
child 20044 92cc2f4c7335
     1.1 --- a/src/HOL/Integ/IntDiv_setup.ML	Fri Sep 23 21:02:13 2005 +0200
     1.2 +++ b/src/HOL/Integ/IntDiv_setup.ML	Fri Sep 23 22:21:49 2005 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  
     1.5  val prove_eq_sums =
     1.6    let val simps = diff_int_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac
     1.7 -  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end
     1.8 +  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
     1.9  
    1.10  end;
    1.11