doc-src/Codegen/Thy/Program.thy

   likely to be used in such situations.
 *}
 
 subsection {* Inductive Predicates *}
 (*<*)
-hide const append
+hide_const append
 
 inductive append
 where
   "append [] ys ys"
 | "append xs ys zs ==> append (x # xs) ys (x # zs)"