src/HOL/IMP/ROOT.ML
changeset 1296 ae31bb7774a7
parent 1165 97b2bb5d43c3
child 1340 71b0a5d83347
     1.1 --- a/src/HOL/IMP/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
     1.2 +++ b/src/HOL/IMP/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
     1.3 @@ -22,3 +22,5 @@
     1.4  time_use_thy "Properties";
     1.5  time_use_thy "Equiv";
     1.6  time_use_thy "Hoare";
     1.7 +
     1.8 +make_chart ();   (*make HTML chart*)