src/Doc/Implementation/Integration.thy

--- a/src/Doc/Implementation/Integration.thy	Thu Dec 04 20:45:11 2014 +0100
+++ b/src/Doc/Implementation/Integration.thy	Thu Dec 04 20:56:38 2014 +0100
@@ -150,6 +150,10 @@
   \end{description}
 \<close>
 
+text %mlex \<open>The file @{"file" "~~/src/HOL/ex/Commands.thy"} shows some example
+Isar command definitions, with the all-important theory header declarations
+for outer syntax keywords.\<close>
+
 
 section \<open>Theory loader database\<close>