--- a/src/Pure/Isar/keyword.scala Wed Sep 11 18:52:30 2013 +0200
+++ b/src/Pure/Isar/keyword.scala Wed Sep 11 20:16:28 2013 +0200
@@ -25,6 +25,7 @@
val THY_SCRIPT = "thy_script"
val THY_GOAL = "thy_goal"
val QED = "qed"
+ val QED_SCRIPT = "qed_script"
val QED_BLOCK = "qed_block"
val QED_GLOBAL = "qed_global"
val PRF_HEADING2 = "prf_heading2"
@@ -53,10 +54,12 @@
val theory1 = Set(THY_BEGIN, THY_END)
val theory2 = Set(THY_DECL, THY_GOAL)
val proof =
- Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL, PRF_BLOCK,
- PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+ Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4,
+ PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL,
+ PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
val proof1 =
- Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
+ Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
+ PRF_CHAIN, PRF_DECL)
val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
val improper = Set(THY_SCRIPT, PRF_SCRIPT)
}