diff --git a/README b/README
deleted file mode 100644
index c77e299e970e0adeed931f3b8d92afc00275321c..0000000000000000000000000000000000000000
--- a/README
+++ /dev/null
@@ -1 +0,0 @@
-Trying to clean the slate.
diff --git a/WISHLIST b/WISHLIST
deleted file mode 100644
index e559aff38d008e642ed1aabeab288ff0fe170623..0000000000000000000000000000000000000000
--- a/WISHLIST
+++ /dev/null
@@ -1,26 +0,0 @@
-Do Add here what you would love FunCheck to be able to do
-------------------------------------------------------
-VK: support maps Map[A,B] for ground types A,B (no polymorphism)
-VK: add bitvectors, including multiplication of int32 variables
-
-PS: support multiple top-level objects
-PS: support tuples (including natively in Z3)
-PS: implement @induct tactic, completely, not just for one arg
-PS: construct models for sets properly (also in interpreter)
-PS: support maps natively
-
-PS: use different levels of summaries (eg. just contract, part of contract
-that's public, then finally body) in unrollings, trying to minimize the
-branching at first
-
-Wishes granted so far
----------------------
-
-PS: create a wishlist
-PS: rewrite pattern-matching translator to use if-then-else
-VK: add IsValid class to allow for writing just "holds" in place of ensuring(_ == true)
-PS: generate VCs for preconditions
-PS: generate VCs for pattern-matching
-PS: use 'private' accessor to indicate what's part of the interface
-PS: use a theory plugin to instantiate/unroll function bodies
-PS: instantiate/unroll function bodies in a fair way, to guarantee termination
diff --git a/funcheck-laraserver b/funcheck-laraserver
deleted file mode 100755
index 418bf2959b3acfc8007d5853e64ffd45ee7d97e9..0000000000000000000000000000000000000000
--- a/funcheck-laraserver
+++ /dev/null
@@ -1,15 +0,0 @@
-#!/bin/bash
-FUNCHECKCLASSPATH="/localhome/liftweb/funcheck/project/boot/scala-2.8.1/lib/scala-library.jar:/localhome/liftweb/funcheck/project/boot/scala-2.8.1/lib/scala-compiler.jar:/localhome/liftweb/funcheck/bin/purescala/purescala-definitions_2.8.1-1.0.jar:/localhome/liftweb/funcheck/bin/funcheck/funcheck-plugin_2.8.1-1.0.jar:/localhome/liftweb/funcheck/lib/z3.jar"
-
-for f in "/localhome/liftweb/funcheck/bin/multisets-lib/multiset-placeholder-library_2.8.1-1.0.jar" "/localhome/liftweb/funcheck/bin/multisets/multiset-solver_2.8.1-1.0.jar" "/localhome/liftweb/funcheck/bin/orderedsets/ordered-sets-solver_2.8.1-1.0.jar" "/localhome/liftweb/funcheck/bin/setconstraints/type-inference-with-set-constraints_2.8.1-1.0.jar"; do
-  if [ -e ${f} ]
-  then
-    FUNCHECKCLASSPATH=${FUNCHECKCLASSPATH}:${f}
-  fi
-done
-
-SCALACCLASSPATH="/localhome/liftweb/funcheck/bin/multisets-lib/multiset-placeholder-library_2.8.1-1.0.jar:/localhome/liftweb/funcheck/bin/funcheck/funcheck-plugin_2.8.1-1.0.jar:/localhome/liftweb/funcheck/bin/purescala/purescala-definitions_2.8.1-1.0.jar"
-
-LD_LIBRARY_PATH=/localhome/liftweb/libstdc++:/localhome/liftweb/z3/z3-2.19/lib \
-scala -classpath ${FUNCHECKCLASSPATH}:${SCALACCLASSPATH} \
-funcheck.Main -cp /localhome/liftweb/funcheck/bin/funcheck/funcheck-plugin_2.8.1-1.0.jar $@