author | nipkow |
Fri, 17 Nov 1995 12:08:04 +0100 | |
changeset 1337 | ad834f39d878 |
parent 1300 | c7a8f374339b |
child 1351 | 4a960c012383 |
permissions | -rw-r--r-- |
(* Title: HOL/MiniML/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1995 TUM Type inference for let-free MiniML *) HOL_build_completed; (*Make examples fail if HOL did*) writeln"Root file for HOL/MiniML"; loadpath := [".","MiniML"]; Unify.trace_bound := 20; time_use_thy "I"; make_chart (); (*make HTML chart*)