(* $Id$ *)

header {* Demonstrate the use of literal command markup *}

theory Sendback imports Main begin

ML {*
fun sendback cmd = ProofGeneral.sendback "Try this:" [Pretty.str cmd]
*}

theorem and_comms: "A & B --> B & A"
proof
  ML {* sendback "assume \"A & B\"" *}
  ML {* sendback "then; show \"B & A\"" *}
  ML {* sendback "proof; assume B and A; then" *}
  ML {* sendback "show ?thesis; ..; qed" *}
  ML {* sendback "qed" *}
qed