aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/isa/message-test.ML
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2008-07-24 09:51:53 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2008-07-24 09:51:53 +0000
commit76d6b0b2b1f039549d308a0d2c478a6b05869af9 (patch)
tree78cc7e13bf290a17e7006a6d4616a8a08e36ce8f /etc/isa/message-test.ML
parent8f8e9388b582ad6d3ee6e1eea842a8d443d4ce89 (diff)
Merge changes from Version4Branch.
Diffstat (limited to 'etc/isa/message-test.ML')
-rw-r--r--etc/isa/message-test.ML16
1 files changed, 0 insertions, 16 deletions
diff --git a/etc/isa/message-test.ML b/etc/isa/message-test.ML
deleted file mode 100644
index 4afd7120..00000000
--- a/etc/isa/message-test.ML
+++ /dev/null
@@ -1,16 +0,0 @@
-(* Testing different kinds of markup in Isabelle output *)
-
-(* ordinary output between prompts *)
-print "ordinary";
-print "ordinary\n"; (* final newline no difference *)
-
-(* eager annotation: displayed as soon as it's seen *)
-writeln "eager to be seen!";
-
-print "more ordinary\n";
-
-Goal "P-->P";
-
-(* C-c RET to here should show eager annotation, as well as
- updating goals buffer properly. *)
-error "something went wrong";