src/Pure/Isar/outer_syntax.ML
changeset 9552 e3981c1f769d
parent 9223 eb752c2fac22
child 9588 96059cbcb0eb
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 07 14:34:26 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 08 01:17:28 2000 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4        val qed: string
     1.5        val qed_block: string
     1.6        val qed_global: string
     1.7 +      val prf_heading: string
     1.8        val prf_goal: string
     1.9        val prf_block: string
    1.10        val prf_open: string
    1.11 @@ -84,6 +85,7 @@
    1.12    val qed = "qed";
    1.13    val qed_block = "qed-block";
    1.14    val qed_global = "qed-global";
    1.15 +  val prf_heading = "proof-heading";
    1.16    val prf_goal = "proof-goal";
    1.17    val prf_block = "proof-block";
    1.18    val prf_open = "proof-open";
    1.19 @@ -95,8 +97,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, qed_global, prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
    1.24 -    prf_asm, prf_asm_goal, prf_script];
    1.25 +    qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close, prf_chain,
    1.26 +    prf_decl, prf_asm, prf_asm_goal, prf_script];
    1.27  end;
    1.28  
    1.29