36   Uncertified terms are often just called terms. One way to construct them is by 

    36   Uncertified terms are often just called terms. One way to construct them is by 

    37   using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example

    37   using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example

    38 

    38 

    39   @{ML_response [display,gray] 

    39   @{ML_response [display,gray] 

    40 "@{term \"(a::nat) + b = c\"}" 

    40 "@{term \"(a::nat) + b = c\"}" 

    42   (Const (\"Groups.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}

    42   (Const (\"Groups.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}

    43 

    43 

    44   constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using 

    44   constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using 

    45   the internal representation corresponding to the datatype @{ML_type_ind "term"}, 

    45   the internal representation corresponding to the datatype @{ML_type_ind "term"}, 

    46   which is defined as follows: 

    46   which is defined as follows: 

  1090 

  1090 

  1091   In order to find a reasonable solution for a unification problem, Isabelle

  1091   In order to find a reasonable solution for a unification problem, Isabelle

  1092   also tries first to solve the problem by higher-order pattern

  1092   also tries first to solve the problem by higher-order pattern

  1093   unification. Only in case of failure full higher-order unification is

  1093   unification. Only in case of failure full higher-order unification is

  1094   called. This function has a built-in bound, which can be accessed and

  1094   called. This function has a built-in bound, which can be accessed and

  1096 

  1096 

  1097   @{ML_response_fake [display,gray]

  1097   @{ML_response_fake [display,gray]

  1099   "Int 60"}

  1099   "Int 60"}

  1100 

  1100 

  1101   If this bound is reached during unification, Isabelle prints out the

  1101   If this bound is reached during unification, Isabelle prints out the

  1102   warning message @{text [quotes] "Unification bound exceeded"} and

  1102   warning message @{text [quotes] "Unification bound exceeded"} and

  1103   plenty of diagnostic information (sometimes annoyingly plenty of 

  1103   plenty of diagnostic information (sometimes annoyingly plenty of 

  1536   this association is fixed. While this is a ``safety-net'' to make sure a

  1536   this association is fixed. While this is a ``safety-net'' to make sure a

  1537   theorem name refers to a particular theorem or collection of theorems, it is 

  1537   theorem name refers to a particular theorem or collection of theorems, it is 

  1538   also a bit too restrictive in cases where a theorem name should refer to a 

  1538   also a bit too restrictive in cases where a theorem name should refer to a 

  1539   dynamically expanding list of theorems (like a simpset). Therefore Isabelle 

  1539   dynamically expanding list of theorems (like a simpset). Therefore Isabelle 

  1540   also implements a mechanism where a theorem name can refer to a custom theorem 

  1540   also implements a mechanism where a theorem name can refer to a custom theorem 

  1542   To see how it works let us assume we defined our own theorem list @{text MyThmList}.

  1542   To see how it works let us assume we defined our own theorem list @{text MyThmList}.

  1543 *}

  1543 *}

  1544 

  1544 

  1545 ML{*structure MyThmList = Generic_Data

  1545 ML{*structure MyThmList = Generic_Data

  1546   (type T = thm list

  1546   (type T = thm list

  1558 setup %gray {* update @{thm TrueI} *}

  1558 setup %gray {* update @{thm TrueI} *}

  1559  

  1559  

  1560 text {*

  1560 text {*

  1561   We can now install the theorem list so that it is visible to the user and 

  1561   We can now install the theorem list so that it is visible to the user and 

  1562   can be refered to by a theorem name. For this need to call 

  1562   can be refered to by a theorem name. For this need to call 

  1564 *}

  1564 *}

  1565 

  1565 

  1566 setup %gray {* 

  1566 setup %gray {* 

  1568 *}

  1568 *}

  1569 

  1569 

  1570 text {*

  1570 text {*

  1571   with a name and a function that accesses the theorem list. Now if the

  1571   with a name and a function that accesses the theorem list. Now if the

  1572   user issues the command

  1572   user issues the command