src/Pure/Isar/outer_syntax.ML
changeset 7104 247e4247b64e
parent 7062 e992884b256d
child 7192 30a67acd0d7e
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 27 21:58:39 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 27 21:58:59 1999 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4        val control: string
     1.5        val diag: string
     1.6        val thy_begin: string
     1.7 +      val thy_switch: string
     1.8        val thy_end: string
     1.9        val thy_heading: string
    1.10        val thy_decl: string
    1.11 @@ -68,6 +69,7 @@
    1.12    val control = "control";
    1.13    val diag = "diag";
    1.14    val thy_begin = "theory-begin";
    1.15 +  val thy_switch = "theory-switch";
    1.16    val thy_end = "theory-end";
    1.17    val thy_heading = "theory-heading";
    1.18    val thy_decl = "theory-decl";
    1.19 @@ -81,8 +83,8 @@
    1.20    val prf_asm = "proof-asm";
    1.21    val prf_script = "proof-script";
    1.22  
    1.23 -  val kinds = [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_goal, qed,
    1.24 -    qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_script];
    1.25 +  val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_goal,
    1.26 +    qed, qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_script];
    1.27  end;
    1.28  
    1.29