| author | nipkow |
| Fri, 24 Oct 1997 11:56:12 +0200 | |
| changeset 3984 | 8fc76a487616 |
| 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";