add doc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/tactic/arith/normalize_bounds_tactic.h

@@ -5,17 +5,34 @@ Module Name:
 
     normalize_bounds_tactic.h
 
-Abstract:
-
-    Replace x with x' + l, when l <= x
-    where x' is a fresh variable.
-    Note that, after the transformation 0 <= x'.
-
 Author:
 
     Leonardo de Moura (leonardo) 2011-10-21.
 
-Revision History:
+Tactic Documentation:
+
+## Tactic normalize-bounds
+
+### Short Description
+
+Replace $x$ with $x' + l$, when $l \leq x$
+where $x'$ is a fresh variable.
+Note that, after the transformation $0 \leq x'$.
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(assert (<= 3 x))
+(assert (<= (+ x y) z))
+(apply normalize-bounds)
+```
+
+### Notes
+
+* supports proofs and cores
 
 --*/
 #pragma once