added K.qed_global;
authorwenzelm
Tue Feb 08 20:13:58 2000 +0100 (2000-02-08)
changeset 82094816ba139574
parent 8208 67d9d52b0b72
child 8210 ca3997312f47
added K.qed_global;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Feb 08 20:12:36 2000 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Feb 08 20:13:58 2000 +0100
     1.3 @@ -29,6 +29,7 @@
     1.4        val thy_goal: string
     1.5        val qed: string
     1.6        val qed_block: string
     1.7 +      val qed_global: string
     1.8        val prf_goal: string
     1.9        val prf_block: string
    1.10        val prf_chain: string
    1.11 @@ -83,6 +84,7 @@
    1.12    val thy_goal = "theory-goal";
    1.13    val qed = "qed";
    1.14    val qed_block = "qed-block";
    1.15 +  val qed_global = "qed-global";
    1.16    val prf_goal = "proof-goal";
    1.17    val prf_block = "proof-block";
    1.18    val prf_chain = "proof-chain";
    1.19 @@ -92,7 +94,8 @@
    1.20    val prf_script = "proof-script";
    1.21  
    1.22    val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_goal,
    1.23 -    qed, qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    1.24 +    qed, qed_block, qed_global, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_asm_goal,
    1.25 +    prf_script];
    1.26  end;
    1.27  
    1.28