changeset 252 | a4dc62a46ee4 |
parent 251 | f04b33ce250f |
child 253 | 132634d24019 |
--- a/Integ/ROOT.ML Tue Oct 24 14:59:17 1995 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* 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*)