177   Remember that at the moment the introduction rules are just strings, and even

   177   Remember that at the moment the introduction rules are just strings, and even

   178   if the predicates and parameters can contain some typing annotations, they

   178   if the predicates and parameters can contain some typing annotations, they

   179   are not yet in any way reflected in the introduction rules. So the task of

   179   are not yet in any way reflected in the introduction rules. So the task of

   180   @{ML add_inductive in SimpleInductivePackage} is to transform the strings

   180   @{ML add_inductive in SimpleInductivePackage} is to transform the strings

   181   into properly typed terms. For this it can use the function 

   181   into properly typed terms. For this it can use the function 

   183   with possible typing annotations and some rule specifications and attempts to

   183   with possible typing annotations and some rule specifications and attempts to

   184   find a type according to the given type constraints and the type constraints

   184   find a type according to the given type constraints and the type constraints

   185   by the surrounding (local theory). However this function is a bit

   185   by the surrounding (local theory). However this function is a bit

   186   too general for our purposes: we want that each introduction rule has only 

   186   too general for our purposes: we want that each introduction rule has only 

   187   name (for example @{text even0} or @{text evenS}), if a name is given at all.

   187   name (for example @{text even0} or @{text evenS}), if a name is given at all.

   189   than one rule. Since it is quite convenient to rely on this function (instead of

   189   than one rule. Since it is quite convenient to rely on this function (instead of

   190   building your own) we just quick ly write a wrapper function that translates

   190   building your own) we just quick ly write a wrapper function that translates

   191   between our specific format and the general format expected by 

   191   between our specific format and the general format expected by 

   193 

   193 

   194   @{ML_chunk [display,gray,linenos] read_specification}

   194   @{ML_chunk [display,gray,linenos] read_specification}

   195 

   195 

   196   It takes a list of constants, a list of rule specifications and a local theory 

   196   It takes a list of constants, a list of rule specifications and a local theory 

   197   as input. Does the transformation of the rule specifications in Line 3; calls

   197   as input. Does the transformation of the rule specifications in Line 3; calls

   285 *}

   285 *}

   286 

   286 

   287 text {*

   287 text {*

   288   During parsing, both predicates and parameters are treated as variables, so

   288   During parsing, both predicates and parameters are treated as variables, so

   289   the lists \verb!preds_syn! and \verb!params_syn! are just appended

   289   the lists \verb!preds_syn! and \verb!params_syn! are just appended

   292   what is required for our package. It allows several rules to be associated

   292   what is required for our package. It allows several rules to be associated

   293   with one name, and the list of rules can be partitioned into several

   293   with one name, and the list of rules can be partitioned into several

   294   sublists. In order for the list \verb!intro_srcs! of introduction rules

   294   sublists. In order for the list \verb!intro_srcs! of introduction rules

   296   have to turn it into a list of singleton lists. This transformation

   296   have to turn it into a list of singleton lists. This transformation

   297   has to be reversed later on by applying the function

   297   has to be reversed later on by applying the function

   298   @{ML [display] "the_single: 'a list -> 'a"}

   298   @{ML [display] "the_single: 'a list -> 'a"}

   299   to the list \verb!specs! containing the parsed introduction rules.

   299   to the list \verb!specs! containing the parsed introduction rules.

   301   of predicates and parameters that contains the inferred types as well.

   301   of predicates and parameters that contains the inferred types as well.

   302   This list has to be chopped into the two lists \verb!preds_syn'! and

   302   This list has to be chopped into the two lists \verb!preds_syn'! and

   303   \verb!params_syn'! for predicates and parameters, respectively.

   303   \verb!params_syn'! for predicates and parameters, respectively.

   304   All variables occurring in a rule but not in the list of variables passed to

   304   All variables occurring in a rule but not in the list of variables passed to

   306   quantifier.

   306   quantifier.

   307 *}

   307 *}

   308 

   308 

   309 text {*

   309 text {*

   310   Finally, @{ML read_specification in Specification} also returns another local theory,

   310   Finally, @{ML read_specification in Specification} also returns another local theory,