diff --git a/CHANGES.md b/CHANGES.md
index 7edcf63be..e54012126 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -2,6 +2,13 @@
 
 ## NEXT
 
+## 0.7.0.0
+
+- New `eliminate` based solver (see ICFP 2017 paper for algorithm)
+- Proof by Logical Evaluation see `tests/proof`
+- SMTLIB2 ADTs to make data constructors injective 
+- Uniformly support polymorphic functions via `apply` and elaborate
+
 ## 0.3.0.0
 
 - Make interpreted mul and div the default, when `solver = z3`
diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal
index be929fda0..82eff3b86 100644
--- a/liquid-fixpoint.cabal
+++ b/liquid-fixpoint.cabal
@@ -1,5 +1,5 @@
 name:                liquid-fixpoint
-version:             0.6.0.1
+version:             0.7.0.1
 Copyright:           2010-17 Ranjit Jhala, University of California, San Diego.
 synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
 homepage:            https://github.com/ucsd-progsys/liquid-fixpoint