aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/isar-keywords.el
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2000-04-17 12:38:17 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2000-04-17 12:38:17 +0000
commita6e9fc1965981005eccbe54737d7d1a690f72065 (patch)
tree57690aa8cf5b674ce80223c0e0ff7784cdc65574 /isar/isar-keywords.el
parent63785c89d08f41689237e0bc6065540ae7a21e8c (diff)
added 'hide';
Diffstat (limited to 'isar/isar-keywords.el')
-rw-r--r--isar/isar-keywords.el1
1 files changed, 1 insertions, 0 deletions
diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el
index 2e3edc7e..7645cce8 100644
--- a/isar/isar-keywords.el
+++ b/isar/isar-keywords.el
@@ -113,6 +113,7 @@
"defer_recdef"
"defs"
"global"
+ "hide"
"inductive"
"inductive_cases"
"judgment"