aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2010-06-28 07:54:27 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2010-06-28 07:54:27 +0000
commitc36244c1320399b40867877fa7d8656fecacf9a0 (patch)
treec44f4837b8a4f67bcb4ced2498460ef35092d310 /etc
parenta4510d1973380ceeb3af221c48ae4b41249bd512 (diff)
Isabelle syntax update
Diffstat (limited to 'etc')
-rw-r--r--etc/isar/BigErrors.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/etc/isar/BigErrors.thy b/etc/isar/BigErrors.thy
index 100eab6a..ec6d5580 100644
--- a/etc/isar/BigErrors.thy
+++ b/etc/isar/BigErrors.thy
@@ -17,4 +17,4 @@ ML {* Output.error_msg (cat_lines (List.tabulate (10000,K "This is a big error m
interactively but does *not* generate an error when
required by another theory, see, BigErrorsNested *)
-end;
+end