added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
% This file was generated by 'rail' from 'CookBook/generated/root.rai'
\rail@t {simpleinductive}
\rail@t {where}
\rail@t {for}
\rail@i {1}{ simpleinductive target? fixes (for fixes)? \\ (where (thmdecl? prop + '|'))? ; }
\rail@o {1}{
\rail@begin{7}{}
\rail@token{simpleinductive}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{target}[]
\rail@endbar
\rail@nont{fixes}[]
\rail@bar
\rail@nextbar{1}
\rail@token{for}[]
\rail@nont{fixes}[]
\rail@endbar
\rail@cr{3}
\rail@bar
\rail@nextbar{4}
\rail@token{where}[]
\rail@plus
\rail@bar
\rail@nextbar{5}
\rail@nont{thmdecl}[]
\rail@endbar
\rail@nont{prop}[]
\rail@nextplus{6}
\rail@cterm{|}[]
\rail@endplus
\rail@endbar
\rail@end
}