1 theory Ind_Interface

     1 theory Ind_Interface

     2 imports "../Base" Simple_Inductive_Package

     2 imports "../Base" Simple_Inductive_Package

     3 begin

     3 begin

     4 

     4 

     6 

     6 

     7 text {*

     7 text {*

     8 

     8 

     9   In order to add a new inductive predicate to a theory with the help of our

     9   In order to add a new inductive predicate to a theory with the help of our

    10   package, the user must \emph{invoke} it. For every package, there are

    10   package, the user must \emph{invoke} it. For every package, there are

    23   the package as a list of terms, which is more robust than handling strings

    23   the package as a list of terms, which is more robust than handling strings

    24   that are lacking the additional structure of terms. These two ways of

    24   that are lacking the additional structure of terms. These two ways of

    25   invoking the package are reflected in its ML programming interface, which

    25   invoking the package are reflected in its ML programming interface, which

    26   consists of two functions:

    26   consists of two functions:

    27 

    27 

    29 *}

    29 *}

    30 

    30 

    31 text {*

    31 text {*

    32   The function for external invocation of the package is called @{ML

    32   The function for external invocation of the package is called @{ML

    33   add_inductive in SimpleInductivePackage}, whereas the one for internal

    33   add_inductive in SimpleInductivePackage}, whereas the one for internal