| author | clasohm |
| Thu, 29 Jun 1995 12:48:48 +0200 | |
| changeset 1165 | 97b2bb5d43c3 |
| parent 1025 | 23190112d369 |
| child 1296 | ae31bb7774a7 |
| permissions | -rw-r--r-- |
| 1165 | 1 |
(* Title: HOL/Integ/ROOT |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
4 |
Copyright 1995 University of Cambridge |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
5 |
|
| 1165 | 6 |
The Integers in HOL (ported from ZF by Riccardo Mattolini) |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
7 |
*) |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
8 |
|
| 1165 | 9 |
HOL_build_completed; (*Cause examples to fail if HOL did*) |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
10 |
|
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
11 |
loadpath := ["Integ"]; |
|
1025
23190112d369
Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
925
diff
changeset
|
12 |
time_use_thy "Integ"; |