diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..50f8e6f05bcc4f32671593006176ecf14ce2b396
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+# Ignore generated top files
+top.lp
diff --git a/prelude/cert_f/prelude.lp b/prelude/cert_f/prelude.lp
deleted file mode 100644
index 3aeb65abf9f1e2ceb1e1758968f0c45556ceffdb..0000000000000000000000000000000000000000
--- a/prelude/cert_f/prelude.lp
+++ /dev/null
@@ -1,2 +0,0 @@
-require prelude.cert_f.booleans prelude.cert_f.equalities
-prelude.cert_f.naturalnumbers prelude.cert_f.notequal
diff --git a/prelude/core/prelude.lp b/prelude/core/prelude.lp
deleted file mode 100644
index 39bb6dbe66c20e695d363bc1e15a98d3135848c3..0000000000000000000000000000000000000000
--- a/prelude/core/prelude.lp
+++ /dev/null
@@ -1,2 +0,0 @@
-require encodings.pvs_core prelude.core.booleans prelude.core.equalities
-prelude.core.notequal prelude.core.if_def
diff --git a/tools/mk_top.sh b/tools/mk_top.sh
new file mode 100755
index 0000000000000000000000000000000000000000..9a00cdfcb3a3765b054de2520a29e3f79f53c063
--- /dev/null
+++ b/tools/mk_top.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+## [./mk_top.sh d] creates a file [d/top.lp] importing all files in [d/]
+
+out="top.lp"
+
+( cd "$1" || exit
+  rm "${out}"
+  for f in *.lp; do
+      p=$(printf '%s/' "$1" | tr -s '/' '.')
+      printf 'require %s%s\n' "${p}" "${f%.lp}" >> "${out}"
+  done )