author | nipkow |
Fri, 17 Mar 2006 22:33:06 +0100 | |
changeset 19285 | dac2c8014253 |
parent 19284 | 4c86109423d5 |
child 19286 | 83404ccd270a |
--- a/src/HOL/arith_data.ML Fri Mar 17 17:38:38 2006 +0100 +++ b/src/HOL/arith_data.ML Fri Mar 17 22:33:06 2006 +0100 @@ -393,7 +393,7 @@ *) val add_rules = [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq, - One_nat_def,isolateSuc, + add_Suc, One_nat_def,isolateSuc, order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one, zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero];