author | lcp |
Thu, 06 Apr 1995 11:27:54 +0200 | |
changeset 241 | b67c8e01ae04 |
parent 217 | b6c0407f203e |
child 243 | 811481779743 |
permissions | -rw-r--r-- |
217 | 1 |
(* Title: HOL/Integ/ROOT |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1995 University of Cambridge |
|
5 |
||
6 |
The Integers in HOL (ported from ZF by Riccardo Mattolini) |
|
7 |
*) |
|
8 |
||
9 |
HOL_build_completed; (*Cause examples to fail if HOL did*) |
|
10 |
||
11 |
loadpath := ["Integ"]; |
|
12 |
time_use_thy "Integ" handle _ => exit 1; |