etc/isar-keywords-ZF.el

     "disable_pr"
     "display_drafts"
     "done"
     "enable_pr"
     "end"
-    "example_proof"
     "exit"
     "extract"
     "extract_type"
     "finalconsts"
     "finally"

 (defconst isar-keywords-theory-script
   '("inductive_cases"))
 
 (defconst isar-keywords-theory-goal
   '("corollary"
-    "example_proof"
     "instance"
     "interpretation"
     "lemma"
     "schematic_corollary"
     "schematic_lemma"