author | paulson |
Wed, 10 May 2000 13:36:27 +0200 (2000-05-10) | |
changeset 8850 | 03cb6625c4a5 |
parent 8849 | f1933a670ae4 |
child 8851 | d816ec3fab28 |
--- a/src/HOL/Integ/NatSimprocs.ML Wed May 10 11:17:01 2000 +0200 +++ b/src/HOL/Integ/NatSimprocs.ML Wed May 10 13:36:27 2000 +0200 @@ -280,6 +280,15 @@ Addsimprocs Nat_Numeral_Simprocs.cancel_numerals; Addsimprocs [Nat_Numeral_Simprocs.combine_numerals]; + +(*If the result is just #1 + ..., replace it by Suc so that primrecs, etc. + will work.*) +Goal "#1 + n = Suc n"; +by Auto_tac; +qed "one_plus_eq_Suc"; +Addsimps [one_plus_eq_Suc]; + + (*examples: print_depth 22; set proof_timing;