removed make_chart;
authorclasohm
Tue Nov 21 12:43:09 1995 +0100 (1995-11-21)
changeset 13514a960c012383
parent 1350 5bf4a54ba25f
child 1352 2e29baa12ae7
removed make_chart;
theories are now read from the current directory (because of use_dir)
src/CCL/ex/ROOT.ML
src/FOL/ex/ROOT.ML
src/FOLP/ex/ROOT.ML
src/HOL/Hoare/ROOT.ML
src/HOL/IMP/ROOT.ML
src/HOL/Integ/ROOT.ML
src/HOL/Lambda/ROOT.ML
src/HOL/Lex/ROOT.ML
src/HOL/MiniML/ROOT.ML
src/HOL/Subst/ROOT.ML
src/HOL/ex/ROOT.ML
src/HOLCF/ex/ROOT.ML
src/HOLCF/explicit_domains/ROOT.ML
src/ZF/AC/ROOT.ML
src/ZF/Coind/ROOT.ML
src/ZF/IMP/ROOT.ML
src/ZF/Resid/ROOT.ML
src/ZF/ex/ROOT.ML
     1.1 --- a/src/CCL/ex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
     1.2 +++ b/src/CCL/ex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
     1.3 @@ -10,13 +10,11 @@
     1.4  
     1.5  writeln"Root file for CCL examples";
     1.6  proof_timing := true;
     1.7 -loadpath := [".", "ex"];
     1.8  
     1.9 -time_use_thy "ex/Nat";
    1.10 -time_use_thy "ex/List";
    1.11 -time_use_thy "ex/Stream";
    1.12 -time_use_thy "ex/Flag";
    1.13 +time_use_thy "Nat";
    1.14 +time_use_thy "List";
    1.15 +time_use_thy "Stream";
    1.16 +time_use_thy "Flag";
    1.17  
    1.18 -make_chart ();   (*make HTML chart*)
    1.19 -
    1.20 +cd "..";
    1.21  maketest"END: Root file for CCL examples";
     2.1 --- a/src/FOL/ex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
     2.2 +++ b/src/FOL/ex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
     2.3 @@ -12,31 +12,30 @@
     2.4  
     2.5  proof_timing := true;
     2.6  
     2.7 -time_use     "ex/intro.ML";
     2.8 -time_use_thy "ex/Nat";
     2.9 -time_use     "ex/foundn.ML";
    2.10 -time_use_thy "ex/Prolog";
    2.11 +time_use     "intro.ML";
    2.12 +time_use_thy "Nat";
    2.13 +time_use     "foundn.ML";
    2.14 +time_use_thy "Prolog";
    2.15  
    2.16  writeln"\n** Intuitionistic examples **\n";
    2.17 -time_use     "ex/int.ML";
    2.18 +time_use     "int.ML";
    2.19  
    2.20  val thy = IFOL.thy  and  tac = Int.fast_tac 1;
    2.21 -time_use     "ex/prop.ML";
    2.22 -time_use     "ex/quant.ML";
    2.23 +time_use     "prop.ML";
    2.24 +time_use     "quant.ML";
    2.25  
    2.26  writeln"\n** Classical examples **\n";
    2.27 -time_use     "ex/mini.ML";
    2.28 -time_use     "ex/cla.ML";
    2.29 -time_use_thy "ex/If";
    2.30 +time_use     "mini.ML";
    2.31 +time_use     "cla.ML";
    2.32 +time_use_thy "If";
    2.33  
    2.34  val thy = FOL.thy  and  tac = Cla.fast_tac FOL_cs 1;
    2.35 -time_use     "ex/prop.ML";
    2.36 -time_use     "ex/quant.ML";
    2.37 +time_use     "prop.ML";
    2.38 +time_use     "quant.ML";
    2.39  
    2.40  writeln"\n** Simplification examples **\n";
    2.41 -time_use_thy "ex/Nat2";
    2.42 -time_use_thy "ex/List";
    2.43 +time_use_thy "Nat2";
    2.44 +time_use_thy "List";
    2.45  
    2.46 -make_chart ();   (*make HTML chart*)
    2.47 -
    2.48 +cd "..";
    2.49  maketest"END: Root file for FOL examples";
     3.1 --- a/src/FOLP/ex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
     3.2 +++ b/src/FOLP/ex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
     3.3 @@ -12,26 +12,25 @@
     3.4  
     3.5  proof_timing := true;
     3.6  
     3.7 -time_use     "ex/intro.ML";
     3.8 -time_use_thy "ex/Nat";
     3.9 -time_use     "ex/foundn.ML";
    3.10 +time_use     "intro.ML";
    3.11 +time_use_thy "Nat";
    3.12 +time_use     "foundn.ML";
    3.13  
    3.14  writeln"\n** Intuitionistic examples **\n";
    3.15 -time_use     "ex/int.ML";
    3.16 +time_use     "int.ML";
    3.17  
    3.18  val thy = IFOLP.thy  and  tac = Int.fast_tac 1;
    3.19 -time_use     "ex/prop.ML";
    3.20 -time_use     "ex/quant.ML";
    3.21 +time_use     "prop.ML";
    3.22 +time_use     "quant.ML";
    3.23  commit();
    3.24  
    3.25  writeln"\n** Classical examples **\n";
    3.26 -time_use     "ex/cla.ML";
    3.27 -time_use_thy "ex/If";
    3.28 +time_use     "cla.ML";
    3.29 +time_use_thy "If";
    3.30  
    3.31  val thy = FOLP.thy  and  tac = Cla.fast_tac FOLP_cs 1;
    3.32 -time_use     "ex/prop.ML";
    3.33 -time_use     "ex/quant.ML";
    3.34 +time_use     "prop.ML";
    3.35 +time_use     "quant.ML";
    3.36  
    3.37 -make_chart ();   (*make HTML chart*)
    3.38 -
    3.39 +cd "..";
    3.40  maketest"END: Root file for FOLP examples";
     4.1 --- a/src/HOL/Hoare/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
     4.2 +++ b/src/HOL/Hoare/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
     4.3 @@ -6,7 +6,4 @@
     4.4  
     4.5  HOL_build_completed;	(*Make examples fail if HOL did*)
     4.6  
     4.7 -loadpath := ["Hoare"];
     4.8  use_thy "Examples";
     4.9 -
    4.10 -make_chart ();   (*make HTML chart*)
     5.1 --- a/src/HOL/IMP/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
     5.2 +++ b/src/HOL/IMP/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
     5.3 @@ -8,9 +8,6 @@
     5.4  
     5.5  writeln"Root file for HOL/IMP";
     5.6  proof_timing := true;
     5.7 -loadpath := [".","IMP"];
     5.8  time_use_thy "Properties";
     5.9  time_use_thy "Equiv";
    5.10  time_use_thy "Hoare";
    5.11 -
    5.12 -make_chart ();   (*make HTML chart*)
     6.1 --- a/src/HOL/Integ/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
     6.2 +++ b/src/HOL/Integ/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
     6.3 @@ -8,7 +8,4 @@
     6.4  
     6.5  HOL_build_completed;    (*Cause examples to fail if HOL did*)
     6.6  
     6.7 -loadpath := ["Integ"];
     6.8  time_use_thy "Integ";
     6.9 -
    6.10 -make_chart ();   (*make HTML chart*)
     7.1 --- a/src/HOL/Lambda/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
     7.2 +++ b/src/HOL/Lambda/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
     7.3 @@ -7,8 +7,5 @@
     7.4  HOL_build_completed;	(*Make examples fail if HOL did*)
     7.5  
     7.6  writeln"Root file for HOL/Lambda";
     7.7 -loadpath := [".","Lambda"];
     7.8  
     7.9  time_use_thy "Eta";
    7.10 -
    7.11 -make_chart ();   (*make HTML chart*)
     8.1 --- a/src/HOL/Lex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
     8.2 +++ b/src/HOL/Lex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
     8.3 @@ -6,8 +6,4 @@
     8.4  
     8.5  HOL_build_completed;	(*Make examples fail if HOL did*)
     8.6  
     8.7 -loadpath := ["Lex"];
     8.8 -
     8.9  use_thy"AutoChopper";
    8.10 -
    8.11 -make_chart ();   (*make HTML chart*)
     9.1 --- a/src/HOL/MiniML/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
     9.2 +++ b/src/HOL/MiniML/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
     9.3 @@ -9,9 +9,6 @@
     9.4  HOL_build_completed;	(*Make examples fail if HOL did*)
     9.5  
     9.6  writeln"Root file for HOL/MiniML";
     9.7 -loadpath := [".","MiniML"];
     9.8  Unify.trace_bound := 20;
     9.9  
    9.10  time_use_thy "I";
    9.11 -
    9.12 -make_chart ();   (*make HTML chart*)
    10.1 --- a/src/HOL/Subst/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
    10.2 +++ b/src/HOL/Subst/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
    10.3 @@ -26,10 +26,7 @@
    10.4  HOL_build_completed;    (*Cause examples to fail if HOL did*)
    10.5  
    10.6  writeln"Root file for Substitutions and Unification";
    10.7 -loadpath := ["Subst"];
    10.8  
    10.9  use_thy "Unifier";
   10.10  
   10.11 -make_chart ();   (*make HTML chart*)
   10.12 -
   10.13  writeln"END: Root file for Substitutions and Unification";
    11.1 --- a/src/HOL/ex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
    11.2 +++ b/src/HOL/ex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
    11.3 @@ -10,10 +10,9 @@
    11.4  
    11.5  writeln "Root file for HOL examples";
    11.6  proof_timing := true;
    11.7 -loadpath := ["ex"];
    11.8 -time_use     "ex/cla.ML";
    11.9 -time_use     "ex/meson.ML";
   11.10 -time_use     "ex/mesontest.ML";
   11.11 +time_use     "cla.ML";
   11.12 +time_use     "meson.ML";
   11.13 +time_use     "mesontest.ML";
   11.14  time_use_thy "String";
   11.15  time_use_thy "BT";
   11.16  time_use_thy "Perm";
   11.17 @@ -22,7 +21,7 @@
   11.18  time_use_thy "LexProd";
   11.19  time_use_thy "Puzzle";
   11.20  time_use_thy "NatSum";
   11.21 -time_use     "ex/set.ML";
   11.22 +time_use     "set.ML";
   11.23  time_use_thy "SList";
   11.24  time_use_thy "LList";
   11.25  time_use_thy "Acc";
   11.26 @@ -31,6 +30,4 @@
   11.27  time_use_thy "Simult";
   11.28  time_use_thy "MT";
   11.29  
   11.30 -make_chart ();   (*make HTML chart*)
   11.31 -
   11.32  writeln "END: Root file for HOL examples";
    12.1 --- a/src/HOLCF/ex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
    12.2 +++ b/src/HOLCF/ex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
    12.3 @@ -10,11 +10,11 @@
    12.4  
    12.5  writeln"Root file for HOLCF examples";
    12.6  proof_timing := true;
    12.7 -time_use_thy "ex/Hoare";
    12.8 -time_use_thy "ex/Loop";
    12.9 -time_use_thy "ex/Fix2";
   12.10 -time_use "ex/loeckx.ML";
   12.11  
   12.12 -make_chart ();   (*make HTML chart*)
   12.13 +time_use_thy "Hoare";
   12.14 +time_use_thy "Loop";
   12.15 +time_use_thy "Fix2";
   12.16 +time_use "loeckx.ML";
   12.17  
   12.18 +cd "..";
   12.19  maketest     "END: Root file for HOLCF examples";
    13.1 --- a/src/HOLCF/explicit_domains/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
    13.2 +++ b/src/HOLCF/explicit_domains/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
    13.3 @@ -9,14 +9,16 @@
    13.4  
    13.5  writeln"Root file for HOLCF examples: explicit domain axiomatisation";
    13.6  proof_timing := true;
    13.7 -time_use_thy "explicit_domains/Dnat";
    13.8 -time_use_thy "explicit_domains/Dnat2";
    13.9 -time_use_thy "explicit_domains/Stream";
   13.10 -time_use_thy "explicit_domains/Stream2";
   13.11 -time_use_thy "explicit_domains/Dlist";
   13.12 +
   13.13 +time_use_thy "Dnat";
   13.14 +time_use_thy "Dnat2";
   13.15 +time_use_thy "Stream";
   13.16 +time_use_thy "Stream2";
   13.17 +time_use_thy "Dlist";
   13.18  
   13.19 -time_use_thy "explicit_domains/Coind";
   13.20 -time_use_thy "explicit_domains/Dagstuhl";
   13.21 -time_use_thy "explicit_domains/Focus_ex";
   13.22 +time_use_thy "Coind";
   13.23 +time_use_thy "Dagstuhl";
   13.24 +time_use_thy "Focus_ex";
   13.25  
   13.26 +cd "..";
   13.27  maketest "END: Root file for HOLCF examples: explicit domain axiomatization";
    14.1 --- a/src/ZF/AC/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
    14.2 +++ b/src/ZF/AC/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
    14.3 @@ -11,35 +11,31 @@
    14.4  writeln"Root file for ZF/AC";
    14.5  proof_timing := true;
    14.6  
    14.7 -loadpath := [".", "AC"];
    14.8 -
    14.9 -time_use_thy "AC/AC_Equiv";
   14.10 +time_use_thy "AC_Equiv";
   14.11  
   14.12 -time_use     "AC/WO1_WO6.ML";
   14.13 -time_use_thy "AC/WO6_WO1";
   14.14 -time_use     "AC/WO1_WO7.ML";
   14.15 -time_use     "AC/WO1_WO8.ML";
   14.16 +time_use     "WO1_WO6.ML";
   14.17 +time_use_thy "WO6_WO1";
   14.18 +time_use     "WO1_WO7.ML";
   14.19 +time_use     "WO1_WO8.ML";
   14.20  
   14.21 -time_use     "AC/AC0_AC1.ML";
   14.22 -time_use     "AC/AC2_AC6.ML";
   14.23 -time_use     "AC/AC7_AC9.ML";
   14.24 +time_use     "AC0_AC1.ML";
   14.25 +time_use     "AC2_AC6.ML";
   14.26 +time_use     "AC7_AC9.ML";
   14.27  
   14.28 -time_use_thy "AC/WO1_AC";
   14.29 -time_use_thy "AC/AC1_WO2";
   14.30 +time_use_thy "WO1_AC";
   14.31 +time_use_thy "AC1_WO2";
   14.32  
   14.33 -time_use     "AC/AC10_AC15.ML";
   14.34 -time_use_thy "AC/AC15_WO6";
   14.35 -
   14.36 -time_use_thy "AC/WO2_AC16";
   14.37 -time_use_thy "AC/AC16_WO4";
   14.38 +time_use     "AC10_AC15.ML";
   14.39 +time_use_thy "AC15_WO6";
   14.40  
   14.41 -time_use     "AC/AC1_AC17.ML";
   14.42 -time_use_thy "AC/AC17_AC1";
   14.43 +time_use_thy "WO2_AC16";
   14.44 +time_use_thy "AC16_WO4";
   14.45  
   14.46 -time_use_thy "AC/AC18_AC19";
   14.47 +time_use     "AC1_AC17.ML";
   14.48 +time_use_thy "AC17_AC1";
   14.49  
   14.50 -time_use_thy "AC/DC";
   14.51 +time_use_thy "AC18_AC19";
   14.52  
   14.53 -make_chart ();   (*make HTML chart*)
   14.54 +time_use_thy "DC";
   14.55  
   14.56  writeln"END: Root file for ZF/AC";
    15.1 --- a/src/ZF/Coind/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
    15.2 +++ b/src/ZF/Coind/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
    15.3 @@ -17,7 +17,5 @@
    15.4  
    15.5  writeln"Root file for ZF/Coind";
    15.6  proof_timing := true;
    15.7 -loadpath     := [".","Coind"];
    15.8 +
    15.9  time_use_thy "MT";
   15.10 -
   15.11 -make_chart ();   (*make HTML chart*)
    16.1 --- a/src/ZF/IMP/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
    16.2 +++ b/src/ZF/IMP/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
    16.3 @@ -16,7 +16,5 @@
    16.4  
    16.5  writeln"Root file for ZF/IMP";
    16.6  proof_timing := true;
    16.7 -loadpath := [".","IMP"];
    16.8 +
    16.9  time_use_thy "Equiv";
   16.10 -
   16.11 -make_chart ();   (*make HTML chart*)
    17.1 --- a/src/ZF/Resid/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
    17.2 +++ b/src/ZF/Resid/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
    17.3 @@ -17,10 +17,6 @@
    17.4  writeln"Root file for ZF/Resid";
    17.5  proof_timing := true;
    17.6  
    17.7 -loadpath := [".", "Resid"];
    17.8 -
    17.9  time_use_thy "Confluence";
   17.10  
   17.11 -make_chart ();   (*make HTML chart*)
   17.12 -
   17.13  writeln"END: Root file for ZF/Resid";
    18.1 --- a/src/ZF/ex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
    18.2 +++ b/src/ZF/ex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
    18.3 @@ -11,37 +11,33 @@
    18.4  writeln"Root file for ZF Set Theory examples";
    18.5  proof_timing := true;
    18.6  
    18.7 -loadpath := [".", "ex"];
    18.8 -
    18.9 -time_use     "ex/misc.ML";
   18.10 -time_use_thy "ex/Ramsey";
   18.11 -time_use_thy "ex/Limit";
   18.12 +time_use     "misc.ML";
   18.13 +time_use_thy "Ramsey";
   18.14 +time_use_thy "Limit";
   18.15  
   18.16  (*Integers & Binary integer arithmetic*)
   18.17 -time_use_thy "ex/Bin";
   18.18 +time_use_thy "Bin";
   18.19  
   18.20  (** Datatypes **)
   18.21 -time_use_thy "ex/BT";		(*binary trees*)
   18.22 -time_use_thy "ex/Data";		(*Sample datatype*)
   18.23 -time_use_thy "ex/Term";		(*terms: recursion over the list functor*)
   18.24 -time_use_thy "ex/TF";		(*trees/forests: mutual recursion*)
   18.25 -time_use_thy "ex/Ntree";	(*variable-branching trees; function demo*)
   18.26 -time_use_thy "ex/Brouwer";	(*Infinite-branching trees*)
   18.27 -time_use_thy "ex/Enum";		(*Enormous enumeration type*)
   18.28 +time_use_thy "BT";		(*binary trees*)
   18.29 +time_use_thy "Data";		(*Sample datatype*)
   18.30 +time_use_thy "Term";		(*terms: recursion over the list functor*)
   18.31 +time_use_thy "TF";		(*trees/forests: mutual recursion*)
   18.32 +time_use_thy "Ntree";		(*variable-branching trees; function demo*)
   18.33 +time_use_thy "Brouwer";		(*Infinite-branching trees*)
   18.34 +time_use_thy "Enum";		(*Enormous enumeration type*)
   18.35  
   18.36  (** Inductive definitions **)
   18.37 -time_use_thy "ex/Rmap";		(*mapping a relation over a list*)
   18.38 -time_use_thy "ex/PropLog";	(*completeness of propositional logic*)
   18.39 +time_use_thy "Rmap";		(*mapping a relation over a list*)
   18.40 +time_use_thy "PropLog";		(*completeness of propositional logic*)
   18.41  (*two Coq examples by Christine Paulin-Mohring*)
   18.42 -time_use_thy "ex/ListN";
   18.43 -time_use_thy "ex/Acc";
   18.44 -time_use_thy "ex/Comb";		(*Combinatory Logic example*)
   18.45 -time_use_thy "ex/Primrec";	(*Primitive recursive functions*)
   18.46 +time_use_thy "ListN";
   18.47 +time_use_thy "Acc";
   18.48 +time_use_thy "Comb";		(*Combinatory Logic example*)
   18.49 +time_use_thy "Primrec";		(*Primitive recursive functions*)
   18.50  
   18.51  (** CoDatatypes **)
   18.52 -time_use_thy "ex/LList";
   18.53 -time_use_thy "ex/CoUnit";
   18.54 -
   18.55 -make_chart ();   (*make HTML chart*)
   18.56 +time_use_thy "LList";
   18.57 +time_use_thy "CoUnit";
   18.58  
   18.59  writeln"END: Root file for ZF Set Theory examples";