diff options
| -rw-r--r-- | etc/isar/BigErrors.thy | 2 |
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 |