diff options
-rw-r--r-- | phox/phox-font.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/phox/phox-font.el b/phox/phox-font.el index 3064a855..5aef6964 100644 --- a/phox/phox-font.el +++ b/phox/phox-font.el @@ -18,7 +18,7 @@ "Sort\\|" "new_\\(intro\\|elim\\|rewrite\\)\\|" "a\\(dd_path\\|uthor\\)\\|" - "c\\(laim\\|ose_def\\|or\\(ollary\\)?\\)\\|" + "c\\(l\\(aim\\|ose_def\\)\\|or\\(ollary\\)?\\)\\|" "d\\(e\\(f\\(_thlist\\)?\\|l\\(_proof\\)\\)\\|ocuments\\|epend\\)\\|" "e\\(lim_after_intro\\|xport\\|del\\|show\\)\\|" "f\\(act\\|lag\\)\\|" |