author | paulson |
Mon, 14 Aug 1995 13:42:27 +0200 | |
changeset 1228 | 7d6b0241afab |
parent 1165 | 97b2bb5d43c3 |
child 1296 | ae31bb7774a7 |
permissions | -rw-r--r-- |
(* Title: HOL/Integ/ROOT ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge The Integers in HOL (ported from ZF by Riccardo Mattolini) *) HOL_build_completed; (*Cause examples to fail if HOL did*) loadpath := ["Integ"]; time_use_thy "Integ";