changeset 5078 | 7b5ea59c0275 |
parent 2280 | eb2ba30c2981 |
5077:71043526295f | 5078:7b5ea59c0275 |
---|---|
4 Copyright 1995 University of Cambridge |
4 Copyright 1995 University of Cambridge |
5 |
5 |
6 The Integers in HOL (ported from ZF by Riccardo Mattolini) |
6 The Integers in HOL (ported from ZF by Riccardo Mattolini) |
7 *) |
7 *) |
8 |
8 |
9 HOL_build_completed; (*Cause examples to fail if HOL did*) |
|
10 |
|
11 time_use_thy "Bin"; |
9 time_use_thy "Bin"; |
12 time_use_thy "IntRing"; |