prf_heading kind;
authorwenzelm
Tue Aug 08 01:17:28 2000 +0200 (2000-08-08)
changeset 9552e3981c1f769d
parent 9551 f4bfb69ae94e
child 9553 c2e3773475b6
prf_heading kind;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Aug 07 14:34:26 2000 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 08 01:17:28 2000 +0200
     1.3 @@ -60,14 +60,14 @@
     1.4    (P.comment >> (Toplevel.theory o IsarThy.add_text_raw));
     1.5  
     1.6  
     1.7 -val sectP = OuterSyntax.markup_command IsarOutput.Markup "sect" "formal comment (proof)" K.prf_decl
     1.8 -  (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));
     1.9 +val sectP = OuterSyntax.markup_command IsarOutput.Markup "sect" "formal comment (proof)"
    1.10 +  K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));
    1.11  
    1.12  val subsectP = OuterSyntax.markup_command IsarOutput.Markup "subsect" "formal comment (proof)"
    1.13 -  K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
    1.14 +  K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
    1.15  
    1.16  val subsubsectP = OuterSyntax.markup_command IsarOutput.Markup "subsubsect"
    1.17 -  "formal comment (proof)" K.prf_decl
    1.18 +  "formal comment (proof)" K.prf_heading
    1.19    (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect)));
    1.20  
    1.21  val txtP = OuterSyntax.markup_command IsarOutput.MarkupEnv "txt" "formal comment (proof)"
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 07 14:34:26 2000 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 08 01:17:28 2000 +0200
     2.3 @@ -30,6 +30,7 @@
     2.4        val qed: string
     2.5        val qed_block: string
     2.6        val qed_global: string
     2.7 +      val prf_heading: string
     2.8        val prf_goal: string
     2.9        val prf_block: string
    2.10        val prf_open: string
    2.11 @@ -84,6 +85,7 @@
    2.12    val qed = "qed";
    2.13    val qed_block = "qed-block";
    2.14    val qed_global = "qed-global";
    2.15 +  val prf_heading = "proof-heading";
    2.16    val prf_goal = "proof-goal";
    2.17    val prf_block = "proof-block";
    2.18    val prf_open = "proof-open";
    2.19 @@ -95,8 +97,8 @@
    2.20    val prf_script = "proof-script";
    2.21  
    2.22    val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_goal,
    2.23 -    qed, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
    2.24 -    prf_asm, prf_asm_goal, prf_script];
    2.25 +    qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close, prf_chain,
    2.26 +    prf_decl, prf_asm, prf_asm_goal, prf_script];
    2.27  end;
    2.28  
    2.29