aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>1999-10-01 18:44:20 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>1999-10-01 18:44:20 +0000
commitec1483c11de67a790d3c75fad2d083b836ca0c9d (patch)
tree47cc7b9d16976c9209009ece5dc8d78a66cb9931 /isar
parent275d38ca5a77ae960504ce9af55d4c0cdf9174d6 (diff)
isar-keywords-proof-asm-goal;
Diffstat (limited to 'isar')
-rw-r--r--isar/isar-keywords.el4
-rw-r--r--isar/isar-syntax.el9
2 files changed, 11 insertions, 2 deletions
diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el
index dadac654..b0833486 100644
--- a/isar/isar-keywords.el
+++ b/isar/isar-keywords.el
@@ -14,6 +14,7 @@
"congs"
"distinct"
"files"
+ "in"
"induction"
"infixl"
"infixr"
@@ -173,6 +174,9 @@
"fix"
"presume"))
+(defconst isar-keywords-proof-asm-goal
+ '("obtain"))
+
(defconst isar-keywords-proof-script
'("apply"
"back"
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index ede306ce..351381b4 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -89,6 +89,10 @@
isar-keywords-proof-chain
isar-keywords-proof-decl))
+(defconst isar-keywords-proof-context
+ (append isar-keywords-proof-asm
+ isar-keywords-proof-asm-goal))
+
(defconst isar-keywords-outline
(append isar-keywords-theory-begin
isar-keywords-theory-heading
@@ -104,7 +108,8 @@
(defconst isar-keywords-indent-open
(append isar-keywords-theory-goal
- isar-keywords-proof-goal))
+ isar-keywords-proof-goal
+ isar-keywords-proof-asm-goal))
(defconst isar-keywords-indent-close
(append isar-keywords-save))
@@ -230,7 +235,7 @@
(cons (proof-ids-to-regexp isar-keywords-theory) 'font-lock-keyword-face)
(cons (proof-ids-to-regexp isar-keywords-proof-enclose) 'font-lock-function-name-face)
(cons (proof-ids-to-regexp isar-keywords-proof) 'font-lock-keyword-face)
- (cons (proof-ids-to-regexp isar-keywords-proof-asm) 'proof-declaration-name-face)
+ (cons (proof-ids-to-regexp isar-keywords-proof-context) 'proof-declaration-name-face)
(cons (proof-ids-to-regexp isar-keywords-proof-script) 'font-lock-reference-face)))
(defvar isar-output-font-lock-keywords-1