src/Pure/Isar/outer_keyword.scala
changeset 29450 ac7f67be7f1f
parent 29449 6e7745d35a30
child 32450 375db037f4d2
equal deleted inserted replaced
29449:6e7745d35a30 29450:ac7f67be7f1f
    33   val PRF_SCRIPT = "proof-script"
    33   val PRF_SCRIPT = "proof-script"
    34 
    34 
    35   val minor = Set(MINOR)
    35   val minor = Set(MINOR)
    36   val control = Set(CONTROL)
    36   val control = Set(CONTROL)
    37   val diag = Set(DIAG)
    37   val diag = Set(DIAG)
    38   val theory0 = Set(THY_BEGIN, THY_SWITCH, THY_END)
    38   val heading = Set(THY_HEADING, PRF_HEADING)
    39   val theory1 = Set(THY_HEADING)
    39   val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
    40   val theory2 = Set(THY_DECL, THY_GOAL)
    40   val theory2 = Set(THY_DECL, THY_GOAL)
    41   val proof1 = Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK, PRF_OPEN,
    41   val proof1 =
    42     PRF_CLOSE, PRF_CHAIN, PRF_DECL)
    42     Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
    43   val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
    43   val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
    44   val improper = Set(THY_SCRIPT, PRF_SCRIPT)
    44   val improper = Set(THY_SCRIPT, PRF_SCRIPT)
    45 }
    45 }
    46 
    46