            "coercions" "classes" "symm" "subst" "refl" "trans" "simp" "congr"
            "notations" "abbreviations" "begin_end_hints" "tactic_hints"
            "reduce_hints" "unfold_hints" "aliases" "eqv"
-           "localrefinfo"))
+           "localrefinfo" "recursor"))
   "lean modifiers")
 (defconst lean-modifiers-regexp
   (regexp-opt lean-modifiers))
+
+
+(defconst lean-tactics
+  '("\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply"
+    "apply" "fapply" "eapply" "rename" "intro" "intros" "all_goals" "fold" "focus" "focus_at"
+    "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
+    "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite"
+    "xrewrite" "krewrite" "blast" "simp" "esimp" "unfold" "change" "check_expr" "contradiction"
+    "exfalso" "split" "existsi" "constructor" "fconstructor" "left" "right" "injection" "congruence" "reflexivity"
+    "symmetry" "transitivity" "state" "induction" "induction_using" "fail" "append"
+    "substvars" "now" "with_options")
+  "lean tactics")
+(defconst lean-tactics-regexp
+  (eval `(rx word-start (or ,@lean-tactics) word-end)))
+
+
 (defconst lean-warnings '("sorry" "exit") "lean warnings")
-(defconst lean-warnings-regexp (eval `(rx word-start (or ,@lean-warnings) word-end)))
+(defconst lean-warnings-regexp
+  (eval `(rx word-start (or ,@lean-warnings) word-end)))
+
 
 (defconst lean-syntax-table
   (let ((st (make-syntax-table)))

                 ?⅋ ?⅌ ?⅍ ?ⅎ ?⅏))
    (modify-syntax-entry ?' "w" st)
    (modify-syntax-entry ?_ "w" st)

    ;; Lean operator chars
    (mapc #'(lambda (ch) (modify-syntax-entry ch "_" st))
          "!#$%&*+.<=>@^|~:")

    ;; Whitespace is whitespace
    (modify-syntax-entry ?\  " " st)

      (2 'font-lock-function-name-face))
     ;; place holder
     (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
     ;; tactics
     ("cases[ \t\n]+[^ \t\n]+[ \t\n]+\\(with\\)" (1 'font-lock-constant-face))
     (,lean-tactics-regexp . 'font-lock-constant-face)
     ;; warnings
     (,lean-warnings-regexp . 'font-lock-warning-face)
     )))

;; Syntax Highlighting for Lean Info Mode
