author  clasohm 
Tue, 21 Nov 1995 12:43:09 +0100  
changeset 1351  4a960c012383 
parent 1296  ae31bb7774a7 
child 1465  5d7a7e439cec 
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; 
1351  13 
time_use "cla.ML"; 
14 
time_use "meson.ML"; 

15 
time_use "mesontest.ML"; 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

31 
time_use_thy "MT"; 
1296  32 

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