equal
deleted
inserted
replaced
1 (* Title: Sequents/LK/Nat |
1 (* Title: Sequents/LK/Nat.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1999 University of Cambridge |
4 Copyright 1999 University of Cambridge |
5 |
|
6 Theory of the natural numbers: Peano's axioms, primitive recursion |
|
7 *) |
5 *) |
8 |
6 |
9 Addsimps [Suc_neq_0]; |
7 Addsimps [Suc_neq_0]; |
10 |
8 |
11 Add_safes [Suc_inject RS L_of_imp]; |
9 Add_safes [Suc_inject RS L_of_imp]; |