changeset 17244 | 0b2ff9541727 |
parent 14981 | e73f8140af78 |
child 19739 | c58ef2aa5430 |
17243:c4ff384ee28f | 17244:0b2ff9541727 |
---|---|
1 (* Title: HOL/IOA/NTP/Lemmas.thy |
1 (* Title: HOL/IOA/NTP/Lemmas.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow & Konrad Slind |
3 Author: Tobias Nipkow & Konrad Slind |
4 |
|
5 Arithmetic lemmas. |
|
6 *) |
4 *) |
7 |
5 |
8 Lemmas = NatArith |
6 theory Lemmas |
7 imports Main |
|
8 begin |
|
9 |
|
10 end |
|
11 |