src/Pure/proof_general.ML
changeset 15289 1d2dba93ef08
parent 15286 b084384960d1
child 15400 50bbdabd7326
equal deleted inserted replaced
15288:9d49290ed885 15289:1d2dba93ef08
   909     | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
   909     | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
   910     | "proof-script"   => markup "proofstep"
   910     | "proof-script"   => markup "proofstep"
   911     | "proof-chain"    => markup "proofstep"
   911     | "proof-chain"    => markup "proofstep"
   912     | "proof-decl"     => markup "proofstep"
   912     | "proof-decl"     => markup "proofstep"
   913     | "proof-asm"      => markup "proofstep"
   913     | "proof-asm"      => markup "proofstep"
   914     | "proof-asm-goal" => markup "proofstep"
   914     | "proof-asm-goal" => (markup "opengoal") @ (empty "openblock")  (* nested proof: obtain *)
   915     | "qed"            => xmls_of_qed (name,markup)
   915     | "qed"            => xmls_of_qed (name,markup)
   916     | "qed-block"      => xmls_of_qed (name,markup)
   916     | "qed-block"      => xmls_of_qed (name,markup)
   917     | "qed-global"     => xmls_of_qed (name,markup)
   917     | "qed-global"     => xmls_of_qed (name,markup)
   918     | other => (* default for anything else is "spuriouscmd", ignored for undo. *)
   918     | other => (* default for anything else is "spuriouscmd", ignored for undo. *)
   919       (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other);
   919       (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other);