# HG changeset patch # User haftmann # Date 1273128231 -7200 # Node ID 842fdcd421598bb7ec09891451de74048ec4500c # Parent 806ea6e282e4673d7fee5947f1e262dcb5673eab constant name access lattice is not in use any longer diff -r 806ea6e282e4 -r 842fdcd42159 doc-src/Locales/Locales/Examples.thy --- 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 (* diff -r 806ea6e282e4 -r 842fdcd42159 doc-src/Locales/Locales/document/Examples.tex --- 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