From 89260fcde1b9d0cdd3555d82711fb210ad61fb33 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 26 May 2009 09:10:38 +0000
Subject: Revise example for Isabelle 2009, showing use of two commands on a
 line.

---
 etc/isar/Sendback.thy | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/etc/isar/Sendback.thy b/etc/isar/Sendback.thy
index ee68b80a..8bfe8492 100644
--- a/etc/isar/Sendback.thy
+++ b/etc/isar/Sendback.thy
@@ -6,13 +6,18 @@ theory Sendback imports Main begin
 
 ML {*
 fun sendback cmd = ProofGeneral.sendback "Try this:" [Pretty.str cmd]
+fun sendback2 cmd1 cmd2 =
+  writeln ("Try: " ^ (Markup.markup Markup.sendback cmd1) ^ " or " ^
+	             (Markup.markup Markup.sendback cmd2))
 *}
 
 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" *}
+  ML_command {* sendback "assume \"A & B\"" *}
+  ML_command {* sendback "show \"B & A\"" *}
+  ML_command {* sendback2 "proof assume B and A then" 
+			  "proof assume A and B then" *}
+  ML_command {* sendback "show ?thesis .. qed" *}
+  ML_command {* sendback "qed" *}
+qed
 qed
-- 
cgit v1.2.3