1063 ML{*val _ = OuterSyntax.local_theory "simple_inductive" 

  1063 ML{*val _ = OuterSyntax.local_theory "simple_inductive" 

  1064               "define inductive predicates"

  1064               "define inductive predicates"

  1065                  OuterKeyword.thy_decl specification*}

  1065                  OuterKeyword.thy_decl specification*}

  1066 

  1066 

  1067 

  1067 

  1069 

  1069 

  1070 text {*

  1070 text {*

  1071   Things to include at the end:

  1071   Things to include at the end:

  1072 

  1072 

  1073   \begin{itemize}

  1073   \begin{itemize}