blob: 5d0ac01907604be3ed4f76de329e88ff37df04d3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* $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
|
