--- hol-light/statements.ml 1970-01-01 01:00:00.000000000 +0100
+++ hol-light-patched/statements.ml 2025-01-18 11:12:11.185279392 +0100
@@ -0,0 +1,15 @@
+let name2pairs acc (name, th) =
+ let acc =
+ if is_conj (concl th) then
+ let fold_fun (no, acc) th = (no + 1, (name ^ "_conjunct" ^ (string_of_int no), th) :: acc) in
+ snd (List.fold_left fold_fun (0, acc) (CONJUNCTS th))
+ else acc
+ in (name, th) :: acc
+;;
+let dump_theorems () =
+ let oc = open_out "theorems" in
+ let all_thms = List.fold_left name2pairs [] !theorems in
+ output_value oc (map (fun (a,b) -> (a, dest_thm b)) all_thms);
+ close_out oc
+;;
+dump_theorems ();;
--- hol-light/stage1.ml 1970-01-01 01:00:00.000000000 +0100
+++ hol-light-patched/stage1.ml 2025-01-18 11:12:11.185279392 +0100
@@ -0,0 +1,4 @@
+#use "hol.ml";;
+#use "update_database.ml";;
+#use "statements.ml";;
+exit 0;;
--- hol-light/stage2.ml 1970-01-01 01:00:00.000000000 +0100
+++ hol-light-patched/stage2.ml 2025-01-18 11:12:11.384276293 +0100
@@ -0,0 +1,3 @@
+#use "hol.ml";;
+stop_recording ();;
+exit 0;;