author  clasohm 
Tue, 24 Oct 1995 14:50:24 +0100  
changeset 1296  ae31bb7774a7 
parent 1174  e57a93d41de0 
child 1351  4a960c012383 
permissions  rwrr 
1165  1 
(* Title: HOL/ex/ROOT 
969  2 
ID: $Id$ 
3 
Author: Tobias Nipkow, Cambridge University Computer Laboratory 

4 
Copyright 1991 University of Cambridge 

5 

6 
Executes miscellaneous examples for HigherOrder Logic. 

7 
*) 

8 

1165  9 
HOL_build_completed; (*Cause examples to fail if HOL did*) 
969  10 

1165  11 
writeln "Root file for HOL examples"; 
1026
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

12 
proof_timing := true; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

13 
loadpath := ["ex"]; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

14 
time_use "ex/cla.ML"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

15 
time_use "ex/meson.ML"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

16 
time_use "ex/mesontest.ML"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

17 
time_use_thy "String"; 
1174  18 
time_use_thy "BT"; 
19 
time_use_thy "Perm"; 

1026
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

20 
time_use_thy "InSort"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

21 
time_use_thy "Qsort"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

22 
time_use_thy "LexProd"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

23 
time_use_thy "Puzzle"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

24 
time_use_thy "NatSum"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

25 
time_use "ex/set.ML"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

26 
time_use_thy "SList"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

27 
time_use_thy "LList"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

28 
time_use_thy "Acc"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

29 
time_use_thy "PropLog"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

30 
time_use_thy "Term"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

31 
time_use_thy "Simult"; 
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset

32 
time_use_thy "MT"; 
1296  33 

34 
make_chart (); (*make HTML chart*) 

35 

1165  36 
writeln "END: Root file for HOL examples"; 