359 "List.lists.Cons", |
359 "List.lists.Cons", |
360 "List.listsE", |
360 "List.listsE", |
361 "Nat.less_one", (*not directional? obscure*) |
361 "Nat.less_one", (*not directional? obscure*) |
362 "Nat.not_gr0", |
362 "Nat.not_gr0", |
363 "Nat.one_eq_mult_iff", (*duplicate by symmetry*) |
363 "Nat.one_eq_mult_iff", (*duplicate by symmetry*) |
364 "NatArith.of_nat_0_eq_iff", |
364 "Nat.of_nat_0_eq_iff", |
365 "NatArith.of_nat_eq_0_iff", |
365 "Nat.of_nat_eq_0_iff", |
366 "NatArith.of_nat_le_0_iff", |
366 "Nat.of_nat_le_0_iff", |
367 "NatSimprocs.divide_le_0_iff_number_of", (*too many clauses*) |
367 "NatSimprocs.divide_le_0_iff_number_of", (*too many clauses*) |
368 "NatSimprocs.divide_less_0_iff_number_of", |
368 "NatSimprocs.divide_less_0_iff_number_of", |
369 "NatSimprocs.equation_minus_iff_1", (*not directional*) |
369 "NatSimprocs.equation_minus_iff_1", (*not directional*) |
370 "NatSimprocs.equation_minus_iff_number_of", (*not directional*) |
370 "NatSimprocs.equation_minus_iff_number_of", (*not directional*) |
371 "NatSimprocs.le_minus_iff_1", (*not directional*) |
371 "NatSimprocs.le_minus_iff_1", (*not directional*) |