changeset 47142 | d64fa2ca54b8 |
parent 47108 | 2a1953f0d20d |
child 47432 | e1576d13e933 |
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Tue Mar 27 12:42:54 2012 +0200 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Tue Mar 27 14:49:56 2012 +0200 @@ -38,8 +38,6 @@ val mod_add_right_eq = @{thm mod_add_right_eq} RS sym; val nat_div_add_eq = @{thm div_add1_eq} RS sym; val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym; -val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2; -val ZDIVISION_BY_ZERO_DIV = @{thm DIVISION_BY_ZERO} RS conjunct1; fun prepare_for_linr sg q fm = let