From fecff511bb9fd00267ad9d0d547a64e012480908 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 14 Aug 2007 14:12:40 +0000
Subject: Add support for sending back literal commands reusing PBP markup
 mechanisms.

---
 etc/isar/Sendback.thy | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 etc/isar/Sendback.thy

(limited to 'etc')

diff --git a/etc/isar/Sendback.thy b/etc/isar/Sendback.thy
new file mode 100644
index 00000000..f14ae72c
--- /dev/null
+++ b/etc/isar/Sendback.thy
@@ -0,0 +1,19 @@
+(* Demonstrate the use of literal command markup *)
+
+theory Sendback imports Main begin
+
+ML {* val pgasciiN = "PGASCII";
+fun special oct =
+  if print_mode_active pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
+  else oct_char oct; 
+fun sendback cmd = writeln ("Try this: \n   " ^ (special "375") ^ cmd ^ "\n\n")
+*}
+
+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
-- 
cgit v1.2.3