aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/Example.thy
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-12 08:36:55 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-12 08:36:55 +0000
commit22ceca15e3811a9a62dacf7b7c3bc0e80f99cd0e (patch)
tree454cfe38d7cdc7c3b300c30bf7ae036c1cf8c093 /isar/Example.thy
parentd55abd121ba1a1c5ac49a52622d5e9cc526337aa (diff)
Remove comment at the end testing feature. See etc/isar/Parsing.thy instead.
Diffstat (limited to 'isar/Example.thy')
-rw-r--r--isar/Example.thy2
1 files changed, 0 insertions, 2 deletions
diff --git a/isar/Example.thy b/isar/Example.thy
index 4cf33e0b..0d7edca7 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -45,5 +45,3 @@ theorem "A & B --> B & A"
done
end
-
-(* comment at the end *)