src/Pure/Isar/outer_syntax.ML
changeset 6868 27ba88d57399
parent 6860 8dc6a1e6fa13
child 7026 69724548fad1
equal deleted inserted replaced
6867:7cb9d3250db7 6868:27ba88d57399
    34       val qed_block: string
    34       val qed_block: string
    35       val prf_goal: string
    35       val prf_goal: string
    36       val prf_block: string
    36       val prf_block: string
    37       val prf_chain: string
    37       val prf_chain: string
    38       val prf_decl: string
    38       val prf_decl: string
       
    39       val prf_asm: string
    39       val prf_script: string
    40       val prf_script: string
    40       val kinds: string list
    41       val kinds: string list
    41     end
    42     end
    42   type token
    43   type token
    43   type parser
    44   type parser
    78   val qed_block = "qed-block";
    79   val qed_block = "qed-block";
    79   val prf_goal = "proof-goal";
    80   val prf_goal = "proof-goal";
    80   val prf_block = "proof-block";
    81   val prf_block = "proof-block";
    81   val prf_chain = "proof-chain";
    82   val prf_chain = "proof-chain";
    82   val prf_decl = "proof-decl";
    83   val prf_decl = "proof-decl";
       
    84   val prf_asm = "proof-asm";
    83   val prf_script = "proof-script";
    85   val prf_script = "proof-script";
    84 
    86 
    85   val kinds = [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_goal, qed,
    87   val kinds = [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_goal, qed,
    86     qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_script];
    88     qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_script];
    87 end;
    89 end;
    88 
    90 
    89 
    91 
    90 (* parsers *)
    92 (* parsers *)
    91 
    93