author | clasohm |
Tue, 24 Oct 1995 14:59:17 +0100 | |
changeset 251 | f04b33ce250f |
parent 243 | 811481779743 |
permissions | -rw-r--r-- |
(* Title: Old_HOL/Integ/ROOT.ML 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"; make_chart (); (*make HTML chart*)