1.1 --- a/src/Pure/Isar/keyword.scala	Fri Mar 16 20:45:47 2012 +0100
     1.2 +++ b/src/Pure/Isar/keyword.scala	Fri Mar 16 21:20:23 2012 +0100
     1.3 @@ -16,7 +16,10 @@
     1.4    val DIAG = "diag"
     1.5    val THY_BEGIN = "thy_begin"
     1.6    val THY_END = "thy_end"
     1.7 -  val THY_HEADING = "thy_heading"
     1.8 +  val THY_HEADING1 = "thy_heading1"
     1.9 +  val THY_HEADING2 = "thy_heading2"
    1.10 +  val THY_HEADING3 = "thy_heading3"
    1.11 +  val THY_HEADING4 = "thy_heading4"
    1.12    val THY_DECL = "thy_decl"
    1.13    val THY_SCRIPT = "thy_script"
    1.14    val THY_GOAL = "thy_goal"
    1.15 @@ -24,7 +27,9 @@
    1.16    val QED = "qed"
    1.17    val QED_BLOCK = "qed_block"
    1.18    val QED_GLOBAL = "qed_global"
    1.19 -  val PRF_HEADING = "prf_heading"
    1.20 +  val PRF_HEADING2 = "prf_heading2"
    1.21 +  val PRF_HEADING3 = "prf_heading3"
    1.22 +  val PRF_HEADING4 = "prf_heading4"
    1.23    val PRF_GOAL = "prf_goal"
    1.24    val PRF_BLOCK = "prf_block"
    1.25    val PRF_OPEN = "prf_open"
    1.26 @@ -42,12 +47,13 @@
    1.27    val control = Set(CONTROL)
    1.28    val diag = Set(DIAG)
    1.29    val theory =
    1.30 -    Set(THY_BEGIN, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL)
    1.31 +    Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
    1.32 +      THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL)
    1.33    val theory1 = Set(THY_BEGIN, THY_END)
    1.34    val theory2 = Set(THY_DECL, THY_GOAL)
    1.35    val proof =
    1.36 -    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK,
    1.37 -      PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT)
    1.38 +    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL,
    1.39 +      PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT)
    1.40    val proof1 =
    1.41      Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
    1.42    val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)