diff --git a/src/tactic/core/der_tactic.h b/src/tactic/core/der_tactic.h
index 01417c08d..555d3108d 100644
--- a/src/tactic/core/der_tactic.h
+++ b/src/tactic/core/der_tactic.h
@@ -13,6 +13,39 @@ Author:
 
     Leonardo de Moura (leonardo) 2012-10-20
 
+Tactic Documentation:
+
+## Tactic der
+
+### Short Description:
+
+The tactic performs _destructive equality resolution_.
+
+### Long Description
+
+Destructive equality resolution replaces bound variables that are
+_solved_ by their solutions in formulas. In short, the destructive
+equality resolution rule takes the form:
+
+```
+   (forall (X Y) (or X /= s C[X])) --> (forall (Y) C[Y])
+```
+
+
+### Example
+ 
+```z3
+  (declare-fun f (Int) Int)
+  (declare-fun p (Int Int) Bool)
+  (assert (forall ((x Int) (y Int)) (or (not (= x (f y))) (p x y))))
+  (apply der)
+```
+
+### Notes
+
+* supports unsat cores, proof terms
+
+
 --*/
 #pragma once
 
diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h
index 1207f3de9..604bcf426 100644
--- a/src/tactic/core/solve_eqs_tactic.h
+++ b/src/tactic/core/solve_eqs_tactic.h
@@ -42,7 +42,7 @@ It also allows solving for uninterpreted constants that only appear in a single
 
 ### Example
 
-```z3
+```
 (declare-const x Int)
 (declare-const y Int)
 (declare-const z Int)