14516

1 
theory GenHOL4Prob = GenHOL4Real:


2 


3 
import_segment "hol4";


4 


5 
setup_dump "../HOL" "HOL4Prob";


6 


7 
append_dump "theory HOL4Prob = HOL4Real:";


8 


9 
import_theory prob_extra;


10 


11 
const_moves


12 
COMPL > GenHOL4Base.pred_set.COMPL;


13 


14 
end_import;


15 


16 
import_theory prob_canon;


17 
end_import;


18 


19 
import_theory boolean_sequence;


20 
end_import;


21 


22 
import_theory prob_algebra;


23 
end_import;


24 


25 
import_theory prob;


26 
end_import;


27 


28 
import_theory prob_pseudo;


29 
end_import;


30 


31 
import_theory prob_indep;


32 
end_import;


33 


34 
import_theory prob_uniform;


35 
end_import;


36 


37 
append_dump "end";


38 


39 
flush_dump;


40 


41 
import_segment "";


42 


43 
end
