author | paulson |
Mon, 02 Feb 1998 12:55:39 +0100 | |
changeset 4593 | 6fc8f224655f |
parent 2280 | eb2ba30c2981 |
child 5078 | 7b5ea59c0275 |
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*) time_use_thy "Bin"; time_use_thy "IntRing";