blob: ee68b80a1176388f72b6fc2addc882baba9fe3eb (
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
|
