# HG changeset patch
# User wenzelm
# Date 1346103436 -7200
# Node ID a0aca6d0498ef00f47d159cd421f9623582337bb
# Parent  c548d26daa8c7bb24327e67b7c292302380a3ba1
more official way to set margin;

diff -r c548d26daa8c -r a0aca6d0498e doc-src/Locales/Examples.thy
--- a/doc-src/Locales/Examples.thy	Mon Aug 27 23:29:45 2012 +0200
+++ b/doc-src/Locales/Examples.thy	Mon Aug 27 23:37:16 2012 +0200
@@ -2,8 +2,6 @@
 imports Main
 begin
 
-pretty_setmargin %invisible 65
-
 (*
 text {* The following presentation will use notation of
   Isabelle's meta logic, hence a few sentences to explain this.
diff -r c548d26daa8c -r a0aca6d0498e doc-src/ROOT
--- a/doc-src/ROOT	Mon Aug 27 23:29:45 2012 +0200
+++ b/doc-src/ROOT	Mon Aug 27 23:37:16 2012 +0200
@@ -123,7 +123,7 @@
     "document/root.tex"
 
 session Locales (doc) in "Locales" = HOL +
-  options [document_variants = "locales"]
+  options [document_variants = "locales", pretty_margin = 65]
   theories
     Examples1
     Examples2