diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2007-08-19 11:19:10 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2007-08-19 11:19:10 +0000 |
| commit | 009b2f163964fd95691913163fd15fb43c84fdc0 (patch) | |
| tree | 9b06b8f67aac838de108f9a55988c43500a45d9d /etc/isar | |
| parent | 346b2bf9593bee26e2d3d4f2319df38a92fe9112 (diff) | |
Test ProofGeneral.sendback
Diffstat (limited to 'etc/isar')
| -rw-r--r-- | etc/isar/Sendback.thy | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/etc/isar/Sendback.thy b/etc/isar/Sendback.thy index f14ae72c..345064a0 100644 --- a/etc/isar/Sendback.thy +++ b/etc/isar/Sendback.thy @@ -6,7 +6,12 @@ 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") +fun sendback cmd = writeln ("Try this: \n " ^ (special "376") ^ cmd ^ (special "377") ^ "\n\n") +*} + +ML {* +fun sendback2 cmd = (writeln "Try this: "; + ProofGeneral.sendback cmd []) *} theorem and_comms: "A & B --> B & A" |