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