--- a/doc-src/Locales/Locales/Examples.thy Wed May 05 15:30:01 2010 +0200
+++ b/doc-src/Locales/Locales/Examples.thy Thu May 06 08:43:51 2010 +0200
@@ -2,7 +2,6 @@
imports Main
begin
-hide_const %invisible Lattices.lattice
pretty_setmargin %invisible 65
(*
--- a/doc-src/Locales/Locales/document/Examples.tex Wed May 05 15:30:01 2010 +0200
+++ b/doc-src/Locales/Locales/document/Examples.tex Thu May 06 08:43:51 2010 +0200
@@ -25,8 +25,6 @@
\endisadeliminvisible
%
\isataginvisible
-\isacommand{hide{\isacharunderscore}const}\isamarkupfalse%
-\ Lattices{\isachardot}lattice\isanewline
\isacommand{pretty{\isacharunderscore}setmargin}\isamarkupfalse%
\ {\isadigit{6}}{\isadigit{5}}%
\endisataginvisible