src/Pure/Isar/outer_syntax.ML
changeset 7676 811022c3837e
parent 7613 fe818734c387
child 7683 e74f43f1d8a3
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Oct 01 20:37:38 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Oct 01 20:38:00 1999 +0200
     1.3 @@ -34,6 +34,7 @@
     1.4        val prf_chain: string
     1.5        val prf_decl: string
     1.6        val prf_asm: string
     1.7 +      val prf_asm_goal: string
     1.8        val prf_script: string
     1.9        val kinds: string list
    1.10      end
    1.11 @@ -82,10 +83,11 @@
    1.12    val prf_chain = "proof-chain";
    1.13    val prf_decl = "proof-decl";
    1.14    val prf_asm = "proof-asm";
    1.15 +  val prf_asm_goal = "proof-asm-goal";
    1.16    val prf_script = "proof-script";
    1.17  
    1.18    val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_goal,
    1.19 -    qed, qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_script];
    1.20 +    qed, qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    1.21  end;
    1.22  
    1.23