src/Pure/Isar/outer_syntax.ML
changeset 9588 96059cbcb0eb
parent 9552 e3981c1f769d
child 10749 afdb47b97317
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 14 14:50:11 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Aug 14 14:50:32 2000 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4        val thy_end: string
     1.5        val thy_heading: string
     1.6        val thy_decl: string
     1.7 +      val thy_script: string
     1.8        val thy_goal: string
     1.9        val qed: string
    1.10        val qed_block: string
    1.11 @@ -81,6 +82,7 @@
    1.12    val thy_end = "theory-end";
    1.13    val thy_heading = "theory-heading";
    1.14    val thy_decl = "theory-decl";
    1.15 +  val thy_script = "theory-script";
    1.16    val thy_goal = "theory-goal";
    1.17    val qed = "qed";
    1.18    val qed_block = "qed-block";
    1.19 @@ -96,9 +98,9 @@
    1.20    val prf_asm_goal = "proof-asm-goal";
    1.21    val prf_script = "proof-script";
    1.22  
    1.23 -  val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_goal,
    1.24 -    qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close, prf_chain,
    1.25 -    prf_decl, prf_asm, prf_asm_goal, prf_script];
    1.26 +  val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script,
    1.27 +    thy_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
    1.28 +    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    1.29  end;
    1.30  
    1.31