summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 11 May 2001 13:49:15 +0200 | |

changeset 11296 | 38a69e5d79fa |

parent 11295 | 66925f23ac7f |

child 11297 | 2d73013f3a41 |

added mult_Suc laws to lin.arith.simpset.
removed Suc n = n + #1 added earlier - #1::nat is not expected by Larry's
simprocs.

src/HOL/Integ/NatSimprocs.ML | file | annotate | diff | comparison | revisions | |

src/HOL/Integ/nat_simprocs.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Integ/NatSimprocs.ML Thu May 10 17:28:40 2001 +0200 +++ b/src/HOL/Integ/NatSimprocs.ML Fri May 11 13:49:15 2001 +0200 @@ -30,8 +30,6 @@ by (asm_full_simp_tac (simpset_of Int.thy addsimps [diff_nat_number_of, less_0_number_of RS sym, neg_number_of_bin_pred_iff_0]) 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset_of Int.thy) 1); qed "Suc_diff_number_of"; (* now redundant because of the inverse_fold simproc

--- a/src/HOL/Integ/nat_simprocs.ML Thu May 10 17:28:40 2001 +0200 +++ b/src/HOL/Integ/nat_simprocs.ML Fri May 11 13:49:15 2001 +0200 @@ -571,10 +571,13 @@ val add_rules = [add_nat_number_of, diff_nat_number_of, mult_nat_number_of, eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less, - (*le_Suc_number_of,le_number_of_Suc, + le_Suc_number_of,le_number_of_Suc, less_Suc_number_of,less_number_of_Suc, - Suc_eq_number_of,eq_number_of_Suc*) - Suc_eq_add_numeral_1, + Suc_eq_number_of,eq_number_of_Suc, + read_instantiate_sg (sign_of(the_context())) + [("m","number_of ?v")] mult_Suc, + read_instantiate_sg (sign_of(the_context())) + [("m","number_of ?v")] mult_Suc_right, eq_number_of_0, eq_0_number_of, less_0_number_of, nat_number_of, Let_number_of, if_True, if_False];