src/HOL/Decision_Procs/cooper_tac.ML
changeset 45654 cf10bde35973
parent 45620 f2a587696afb
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sun Nov 27 23:06:59 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sun Nov 27 23:10:19 2011 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5  val nT = HOLogic.natT;
     1.6  val binarith = @{thms normalize_bin_simps};
     1.7 -val comp_arith = binarith @ simp_thms
     1.8 +val comp_arith = binarith @ @{thms simp_thms};
     1.9  
    1.10  val zdvd_int = @{thm zdvd_int};
    1.11  val zdiff_int_split = @{thm zdiff_int_split};