equal
deleted
inserted
replaced
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 2000 University of Cambridge |
4 Copyright 2000 University of Cambridge |
5 |
5 |
6 Simprocs for nat numerals (see also nat_simprocs.ML). |
6 Simprocs for nat numerals (see also nat_simprocs.ML). |
7 *) |
7 *) |
|
8 |
|
9 val ss_Int = simpset_of Int_thy; |
8 |
10 |
9 (** For simplifying Suc m - #n **) |
11 (** For simplifying Suc m - #n **) |
10 |
12 |
11 Goal "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"; |
13 Goal "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"; |
12 by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1] |
14 by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1] |