--- a/CookBook/Package/Ind_Interface.thy Fri Feb 13 01:05:09 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy Fri Feb 13 01:05:31 2009 +0000
@@ -2,7 +2,7 @@
imports "../Base" Simple_Inductive_Package
begin
-section{* The Interface \label{sec:ind-interface} *}
+section {* The Interface \label{sec:ind-interface} *}
text {*
@@ -25,7 +25,7 @@
invoking the package are reflected in its ML programming interface, which
consists of two functions:
- @{ML_chunk [display] SIMPLE_INDUCTIVE_PACKAGE}
+ @{ML_chunk [display,gray] SIMPLE_INDUCTIVE_PACKAGE}
*}
text {*