diff options
| -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" |