diff --git a/Tactic.lp b/Tactic.lp
index 13f54fd..6d4597e 100644
--- a/Tactic.lp
+++ b/Tactic.lp
@@ -46,7 +46,7 @@ builtin "remove" ≔ #remove;
 constant symbol #repeat : Tactic → Tactic;
 builtin "repeat" ≔ #repeat;
 
-constant symbol #rewrite [p] : π p → Tactic;
+ symbol #rewrite : String → String → Π [a], π a → Tactic;
 builtin "rewrite" ≔ #rewrite;
 
 constant symbol #set : String → Π [a], τ a → Tactic;
@@ -70,6 +70,9 @@ builtin "try" ≔ #try;
 constant symbol #why3 : Tactic;
 builtin "why3" ≔ #why3;
 
+constant symbol #change : Tactic;
+builtin "change" ≔ #change;
+
 // defined tactics
 
 symbol nothing ≔ #try #fail;