etc/isar-keywords-ZF.el

     "ultimately"
     "undo"
     "undos_proof"
     "unfolding"
     "unused_thms"
-    "use"
     "use_thy"
     "using"
     "welcome"
     "with"
     "write"

     "theorems"
     "translations"
     "type_notation"
     "type_synonym"
     "typed_print_translation"
-    "typedecl"
-    "use"))
+    "typedecl"))
 
 (defconst isar-keywords-theory-script
   '("inductive_cases"))
 
 (defconst isar-keywords-theory-goal