aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMakarius Wenzel2000-04-17 12:38:17 +0000
committerMakarius Wenzel2000-04-17 12:38:17 +0000
commita6e9fc1965981005eccbe54737d7d1a690f72065 (patch)
tree57690aa8cf5b674ce80223c0e0ff7784cdc65574
parent63785c89d08f41689237e0bc6065540ae7a21e8c (diff)
added 'hide';
-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"