# 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