diff -r 86f2daf48a3c -r a183dec876ab src/HOL/Import/Generate-HOL/GenHOL4Prob.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Fri Apr 02 17:37:45 2004 +0200
@@ -0,0 +1,43 @@
+theory GenHOL4Prob = GenHOL4Real:
+
+import_segment "hol4";
+
+setup_dump "../HOL" "HOL4Prob";
+
+append_dump "theory HOL4Prob = HOL4Real:";
+
+import_theory prob_extra;
+
+const_moves
+  COMPL > GenHOL4Base.pred_set.COMPL;
+
+end_import;
+
+import_theory prob_canon;
+end_import;
+
+import_theory boolean_sequence;
+end_import;
+
+import_theory prob_algebra;
+end_import;
+
+import_theory prob;
+end_import;
+
+import_theory prob_pseudo;
+end_import;
+
+import_theory prob_indep;
+end_import;
+
+import_theory prob_uniform;
+end_import;
+
+append_dump "end";
+
+flush_dump;
+
+import_segment "";
+
+end