diff options
author | Makarius Wenzel <makarius@sketis.net> | 2007-08-20 09:38:10 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 2007-08-20 09:38:10 +0000 |
commit | fdcd31d4ef474b4a7217aa65c239e6e271a35754 (patch) | |
tree | 480e90d9046b603df81c162160cd8c6e5f24f12b /etc/isar | |
parent | 2f5e3825d4c1a38e9334b2a46716e06eb08b3c4f (diff) |
proper use of ProofGeneral.sendback;
Diffstat (limited to 'etc/isar')
-rw-r--r-- | etc/isar/Sendback.thy | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/etc/isar/Sendback.thy b/etc/isar/Sendback.thy index 345064a0..5d0ac019 100644 --- a/etc/isar/Sendback.thy +++ b/etc/isar/Sendback.thy @@ -1,17 +1,11 @@ -(* Demonstrate the use of literal command markup *) +(* $Id$ *) -theory Sendback imports Main begin +header {* Demonstrate the use of literal command markup *} -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 "376") ^ cmd ^ (special "377") ^ "\n\n") -*} +theory Sendback imports Main begin ML {* -fun sendback2 cmd = (writeln "Try this: "; - ProofGeneral.sendback cmd []) +fun sendback cmd = ProofGeneral.sendback "Try this:" [Pretty.str cmd] *} theorem and_comms: "A & B --> B & A" |