doc-src/TutorialI/Documents/Documents.thy
changeset 36176 3fe7e97ccca8
parent 30649 57753e0ec1d4
child 38765 5aa8e5e770a8
--- a/doc-src/TutorialI/Documents/Documents.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -138,7 +138,7 @@
 *}
 
 (*<*)
-hide const xor
+hide_const xor
 setup {* Sign.add_path "version1" *}
 (*>*)
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
@@ -161,7 +161,7 @@
 *}
 
 (*<*)
-hide const xor
+hide_const xor
 setup {* Sign.add_path "version2" *}
 (*>*)
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)