# HG changeset patch # User clasohm # Date 814543109 -3600 # Node ID 488593372568e06f4749b225cd7b6ae50f85a297 # Parent 7ac266cf82d08b9ac34585593144c8fabf4ce736 added call of make_chart diff -r 7ac266cf82d0 -r 488593372568 src/HOL/IOA/ROOT_ABP.ML --- a/src/HOL/IOA/ROOT_ABP.ML Tue Oct 24 14:58:02 1995 +0100 +++ b/src/HOL/IOA/ROOT_ABP.ML Tue Oct 24 14:58:29 1995 +0100 @@ -32,3 +32,5 @@ loadpath := ["IOA/meta_theory","IOA/ABP"]; use_thy "Correctness"; + +make_chart (); (*make HTML chart*) diff -r 7ac266cf82d0 -r 488593372568 src/HOL/IOA/ROOT_NTP.ML --- a/src/HOL/IOA/ROOT_NTP.ML Tue Oct 24 14:58:02 1995 +0100 +++ b/src/HOL/IOA/ROOT_NTP.ML Tue Oct 24 14:58:29 1995 +0100 @@ -32,3 +32,5 @@ loadpath := ["IOA/meta_theory","IOA/NTP"]; use_thy "Correctness"; + +make_chart (); (*make HTML chart*) diff -r 7ac266cf82d0 -r 488593372568 src/LK/ex/ROOT.ML --- a/src/LK/ex/ROOT.ML Tue Oct 24 14:58:02 1995 +0100 +++ b/src/LK/ex/ROOT.ML Tue Oct 24 14:58:29 1995 +0100 @@ -15,4 +15,6 @@ time_use "ex/quant.ML"; time_use "ex/hardquant.ML"; +make_chart (); (*make HTML chart*) + maketest"END: Root file for LK examples";