author  wenzelm 
Sun, 16 Jan 2011 15:53:03 +0100  
changeset 41589  bbd861837ebc 
parent 17566  484ff733f29c 
child 46780  ab4f3f765f91 
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 
41589  2 
Author: Sebastian Skalberg, TU Muenchen 
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

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

4 

16417  5 
theory GenHOL4Prob imports GenHOL4Real begin 
14516  6 

7 
import_segment "hol4"; 

8 

9 
setup_dump "../HOL" "HOL4Prob"; 

10 

17566  11 
append_dump "theory HOL4Prob imports HOL4Real begin"; 
14516  12 

13 
import_theory prob_extra; 

14 

15 
const_moves 

16 
COMPL > GenHOL4Base.pred_set.COMPL; 

17 

18 
end_import; 

19 

20 
import_theory prob_canon; 

21 
end_import; 

22 

23 
import_theory boolean_sequence; 

24 
end_import; 

25 

26 
import_theory prob_algebra; 

27 
end_import; 

28 

29 
import_theory prob; 

30 
end_import; 

31 

32 
import_theory prob_pseudo; 

33 
end_import; 

34 

35 
import_theory prob_indep; 

36 
end_import; 

37 

38 
import_theory prob_uniform; 

39 
end_import; 

40 

41 
append_dump "end"; 

42 

43 
flush_dump; 

44 

45 
import_segment ""; 

46 

47 
end 