changeset 1335 | 5e1c0540f285 |
child 1351 | 4a960c012383 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hoare/ROOT.ML Fri Nov 17 09:04:10 1995 +0100 @@ -0,0 +1,12 @@ +(* Title: HOL/IMP/ROOT.ML + ID: $Id$ + Author: Tobias Nipkow + Copyright 1995 TUM +*) + +HOL_build_completed; (*Make examples fail if HOL did*) + +loadpath := ["Hoare"]; +use_thy "Examples"; + +make_chart (); (*make HTML chart*)