author | clasohm |
Fri, 03 Mar 1995 12:04:45 +0100 | |
changeset 925 | 15539deb6863 |
child 1025 | 23190112d369 |
permissions | -rw-r--r-- |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
1 |
(* Title: CHOL/Integ/ROOT |
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 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
6 |
The Integers in CHOL (ported from ZF by Riccardo Mattolini) |
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 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
9 |
CHOL_build_completed; (*Cause examples to fail if CHOL did*) |
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"]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
12 |
time_use_thy "Integ" handle _ => exit 1; |