1 theory Ind_Code

     2 imports "../Base" Simple_Inductive_Package

     3 begin

     4 

     5 text {*

     6 

     7   @{ML_chunk [display,gray] induction_rules}

     8 

     9 *}

    10 

    11 text {*

    12 

    13   @{ML_chunk [display,gray] intro_rules}

    14 

    15 *}

    16 

    17 text {*

    18 

    19   @{ML_chunk [display,gray] storing}

    20 

    21 *}

    22 end