     "done"
     "enable_pr"
     "end"
+    "enriched_type"
     "equivariance"
     "exit"
     "export_code"

    "code_pred"
    "corollary"
    "cpodef"
    "function"
    "instance"
    "interpretation"

    "sublocale"
    "termination"
    "theorem"
    "typedef"))

(defconst isar-keywords-qed
