src/Pure/Isar/keyword.scala
changeset 69913 ca515cf61651
parent 67090 0ec94bb9cec4
child 69917 66c4567664b5
     1.1 --- a/src/Pure/Isar/keyword.scala	Thu Mar 14 16:35:58 2019 +0100
     1.2 +++ b/src/Pure/Isar/keyword.scala	Thu Mar 14 16:55:06 2019 +0100
     1.3 @@ -21,8 +21,12 @@
     1.4    val THY_END = "thy_end"
     1.5    val THY_DECL = "thy_decl"
     1.6    val THY_DECL_BLOCK = "thy_decl_block"
     1.7 +  val THY_DEFN = "thy_defn"
     1.8 +  val THY_STMT = "thy_stmt"
     1.9    val THY_LOAD = "thy_load"
    1.10    val THY_GOAL = "thy_goal"
    1.11 +  val THY_GOAL_DEFN = "thy_goal_defn"
    1.12 +  val THY_GOAL_STMT = "thy_goal_stmt"
    1.13    val QED = "qed"
    1.14    val QED_SCRIPT = "qed_script"
    1.15    val QED_BLOCK = "qed_block"
    1.16 @@ -60,11 +64,15 @@
    1.17  
    1.18    val theory_load = Set(THY_LOAD)
    1.19  
    1.20 -  val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
    1.21 +  val theory =
    1.22 +    Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_DEFN, THY_STMT,
    1.23 +      THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT)
    1.24  
    1.25    val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
    1.26  
    1.27 -  val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
    1.28 +  val theory_body =
    1.29 +    Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_DEFN, THY_STMT,
    1.30 +      THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT)
    1.31  
    1.32    val prf_script = Set(PRF_SCRIPT)
    1.33  
    1.34 @@ -78,7 +86,7 @@
    1.35        PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
    1.36        PRF_SCRIPT_ASM_GOAL)
    1.37  
    1.38 -  val theory_goal = Set(THY_GOAL)
    1.39 +  val theory_goal = Set(THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT)
    1.40    val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL)
    1.41    val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
    1.42    val qed_global = Set(QED_GLOBAL)