src/HOL/Tools/res_atp.ML
changeset 21243 afffe1f72143
parent 21224 f86b8463af37
child 21290 33b6bb5d6ab8
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Nov 08 11:23:09 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Nov 08 13:48:29 2006 +0100
     1.3 @@ -361,9 +361,9 @@
     1.4     "Nat.less_one", (*not directional? obscure*)
     1.5     "Nat.not_gr0",
     1.6     "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
     1.7 -   "NatArith.of_nat_0_eq_iff",
     1.8 -   "NatArith.of_nat_eq_0_iff",
     1.9 -   "NatArith.of_nat_le_0_iff",
    1.10 +   "Nat.of_nat_0_eq_iff",
    1.11 +   "Nat.of_nat_eq_0_iff",
    1.12 +   "Nat.of_nat_le_0_iff",
    1.13     "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
    1.14     "NatSimprocs.divide_less_0_iff_number_of",
    1.15     "NatSimprocs.equation_minus_iff_1",  (*not directional*)