qed_block keywords;
authorwenzelm
Wed May 26 22:43:27 1999 +0200 (1999-05-26 ago)
changeset 6733429bbd7ef26d
parent 6732 cf9f66ca9ee3
child 6734 151c07f5b70a
qed_block keywords;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed May 26 16:51:05 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed May 26 22:43:27 1999 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4        val thy_decl: string
     1.5        val thy_goal: string
     1.6        val qed: string
     1.7 +      val qed_block: string
     1.8        val prf_goal: string
     1.9        val prf_block: string
    1.10        val prf_chain: string
    1.11 @@ -70,6 +71,7 @@
    1.12    val thy_decl = "theory-decl";
    1.13    val thy_goal = "theory-goal";
    1.14    val qed = "qed";
    1.15 +  val qed_block = "qed-block";
    1.16    val prf_goal = "proof-goal";
    1.17    val prf_block = "proof-block";
    1.18    val prf_chain = "proof-chain";
    1.19 @@ -77,7 +79,7 @@
    1.20    val prf_script = "proof-script";
    1.21  
    1.22    val kinds = [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_goal, qed,
    1.23 -    prf_goal, prf_block, prf_chain, prf_decl, prf_script];
    1.24 +    qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_script];
    1.25  end;
    1.26  
    1.27