diff --git a/src/tactic/core/propagate_values2_tactic.h b/src/tactic/core/propagate_values2_tactic.h
index 4c89fae9766..e380ce7d382 100644
--- a/src/tactic/core/propagate_values2_tactic.h
+++ b/src/tactic/core/propagate_values2_tactic.h
@@ -5,14 +5,41 @@ Module Name:
 
     propagate_values2_tactic.h
 
-Abstract:
-
-    Tactic for propagating equalities (= t v) where v is a value
-
 Author:
 
     Nikolaj Bjorner (nbjorner) 2022-11-24
 
+Tactic Documentation:
+
+## Tactic propagate-values
+
+### Short Description:
+
+Tactic for propagating equalities `(= t v)` where `v` is a value
+
+### Long Description
+
+In a context where terms are equated to constants it is invariably beneficial to 
+replace terms, that can be compound, with the constants and then simplify the resulting formulas.
+The propagate-values tactic accomplishes the task of replacing such terms.
+
+### Example
+ 
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-fun f (Int) Int)
+(assert (= 1 (f (+ x y))))
+(assert (= 2 x))
+(assert (> (f (+ 2 y)) y))
+(apply propagate-values)
+```
+
+### Notes
+
+* supports unsat cores
+
+
 --*/
 #pragma once
 
diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h
index fc262f99859..39e3e9bdeec 100644
--- a/src/tactic/core/simplify_tactic.h
+++ b/src/tactic/core/simplify_tactic.h
@@ -13,7 +13,37 @@ Module Name:
 
     Leonardo (leonardo) 2011-11-20
 
-Notes:
+Tactic Documentation:
+
+## Tactic simplify
+
+### Short Description:
+
+The tactic performs algebraic simplifcations on formulas
+
+### Long Description
+
+The simplify tactic invokes z3's main rewriting engine. 
+The rewriting engine contains support for theory specific simplifications.
+The set of simplifications invoked is open ended. Useful algebraic simplifications
+are added to the rewrite engine as they are discovered to be useful.
+
+Note that the simplifier does not ensure that equivalent formulas are simplified to the same form.
+In other words it does not guarantee canonicity. This contrasts with BDD packages where BDDs constructed
+from two equivalent formulas are guaranteed to be equal.
+
+### Example
+ 
+```z3
+  (declare-const x Int)
+  (declare-const y Int)
+  (assert (> x (+ x y)))
+  (apply simplify)
+```
+
+### Notes
+
+* supports unsat cores, proof terms
 
 --*/
 #pragma once