prf_open/close;
authorwenzelm
Thu Jun 08 21:53:44 2000 +0200 (2000-06-08)
changeset 90568f78b2aea39e
parent 9055 f020e00c6304
child 9057 af1ca1acf292
prf_open/close;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jun 07 17:14:58 2000 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Jun 08 21:53:44 2000 +0200
     1.3 @@ -348,11 +348,11 @@
     1.4  (* proof structure *)
     1.5  
     1.6  val beginP =
     1.7 -  OuterSyntax.command "{" "begin explicit proof block" K.prf_block
     1.8 +  OuterSyntax.command "{" "begin explicit proof block" K.prf_open
     1.9      (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.begin_block)));
    1.10  
    1.11  val endP =
    1.12 -  OuterSyntax.command "}" "end explicit proof block" K.prf_block
    1.13 +  OuterSyntax.command "}" "end explicit proof block" K.prf_close
    1.14      (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.end_block)));
    1.15  
    1.16  val nextP =
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Jun 07 17:14:58 2000 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Jun 08 21:53:44 2000 +0200
     2.3 @@ -33,6 +33,8 @@
     2.4        val qed_global: string
     2.5        val prf_goal: string
     2.6        val prf_block: string
     2.7 +      val prf_open: string
     2.8 +      val prf_close: string
     2.9        val prf_chain: string
    2.10        val prf_decl: string
    2.11        val prf_asm: string
    2.12 @@ -90,6 +92,8 @@
    2.13    val qed_global = "qed-global";
    2.14    val prf_goal = "proof-goal";
    2.15    val prf_block = "proof-block";
    2.16 +  val prf_open = "proof-open";
    2.17 +  val prf_close = "proof-close";
    2.18    val prf_chain = "proof-chain";
    2.19    val prf_decl = "proof-decl";
    2.20    val prf_asm = "proof-asm";
    2.21 @@ -97,8 +101,8 @@
    2.22    val prf_script = "proof-script";
    2.23  
    2.24    val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_goal,
    2.25 -    qed, qed_block, qed_global, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_asm_goal,
    2.26 -    prf_script];
    2.27 +    qed, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
    2.28 +    prf_asm, prf_asm_goal, prf_script];
    2.29  end;
    2.30  
    2.31