Add support for sending back literal commands reusing PBP markup mechanisms.

1 files changed, 19 insertions, 0 deletions

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