author  haftmann 
Fri, 17 Jun 2005 16:12:49 +0200  
changeset 16417  9bc16273c2d4 
parent 14620  1be590fd2422 
child 17566  484ff733f29c 
permissions  rwrr 
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

1 
(* Title: HOL/Import/GenerateHOL/GenHOL4Prob.thy 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

2 
ID: $Id$ 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

3 
Author: Sebastian Skalberg (TU Muenchen) 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

4 
*) 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

5 

16417  6 
theory GenHOL4Prob imports GenHOL4Real begin 
14516  7 

8 
import_segment "hol4"; 

9 

10 
setup_dump "../HOL" "HOL4Prob"; 

11 

12 
append_dump "theory HOL4Prob = HOL4Real:"; 

13 

14 
import_theory prob_extra; 

15 

16 
const_moves 

17 
COMPL > GenHOL4Base.pred_set.COMPL; 

18 

19 
end_import; 

20 

21 
import_theory prob_canon; 

22 
end_import; 

23 

24 
import_theory boolean_sequence; 

25 
end_import; 

26 

27 
import_theory prob_algebra; 

28 
end_import; 

29 

30 
import_theory prob; 

31 
end_import; 

32 

33 
import_theory prob_pseudo; 

34 
end_import; 

35 

36 
import_theory prob_indep; 

37 
end_import; 

38 

39 
import_theory prob_uniform; 

40 
end_import; 

41 

42 
append_dump "end"; 

43 

44 
flush_dump; 

45 

46 
import_segment ""; 

47 

48 
end 