42 

    42 

    43   Like normal Isabelle proof scripts, \isacommand{ML}-commands can be

    43   Like normal Isabelle proof scripts, \isacommand{ML}-commands can be

    44   evaluated by using the advance and undo buttons of your Isabelle

    44   evaluated by using the advance and undo buttons of your Isabelle

    45   environment. The code inside the \isacommand{ML}-command can also contain

    45   environment. The code inside the \isacommand{ML}-command can also contain

    46   value and function bindings, and even those can be undone when the proof

    46   value and function bindings, and even those can be undone when the proof

    48   \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we

    48   \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we

    49   show code. The lines prefixed with @{text [quotes] ">"} are not part of the

    49   show code. The lines prefixed with @{text [quotes] ">"} are not part of the

    50   code, rather they indicate what the response is when the code is evaluated.

    50   code, rather they indicate what the response is when the code is evaluated.

    51 

    51 

    52   Once a portion of code is relatively stable, you usually want to export it

    52   Once a portion of code is relatively stable, you usually want to export it

    71 

    71 

    72   During development you might find it necessary to inspect some data

    72   During development you might find it necessary to inspect some data

    73   in your code. This can be done in a ``quick-and-dirty'' fashion using 

    73   in your code. This can be done in a ``quick-and-dirty'' fashion using 

    74   the function @{ML "warning"}. For example 

    74   the function @{ML "warning"}. For example 

    75 

    75 

    77 

    77 

    78   will print out @{text [quotes] "any string"} inside the response buffer

    78   will print out @{text [quotes] "any string"} inside the response buffer

    79   of Isabelle.  This function expects a string as argument. If you develop under PolyML,

    79   of Isabelle.  This function expects a string as argument. If you develop under PolyML,

    80   then there is a convenient, though again ``quick-and-dirty'', method for

    80   then there is a convenient, though again ``quick-and-dirty'', method for

    81   converting values into strings, namely the function @{ML makestring}:

    81   converting values into strings, namely the function @{ML makestring}:

    82 

    82 

    84 

    84 

    85   However @{ML makestring} only works if the type of what is converted is monomorphic 

    85   However @{ML makestring} only works if the type of what is converted is monomorphic 

    86   and not a function.

    86   and not a function.

    87 

    87 

    88   The function @{ML "warning"} should only be used for testing purposes, because any

    88   The function @{ML "warning"} should only be used for testing purposes, because any

    89   output this function generates will be overwritten as soon as an error is

    89   output this function generates will be overwritten as soon as an error is

    90   raised. For printing anything more serious and elaborate, the

    90   raised. For printing anything more serious and elaborate, the

    91   function @{ML tracing} is more appropriate. This function writes all output into

    91   function @{ML tracing} is more appropriate. This function writes all output into

    92   a separate tracing buffer. For example:

    92   a separate tracing buffer. For example:

    93 

    93 

    95 

    95 

    96   It is also possible to redirect the ``channel'' where the string @{text "foo"} is 

    96   It is also possible to redirect the ``channel'' where the string @{text "foo"} is 

    97   printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive 

    97   printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive 

    98   amounts of trace output. This redirection can be achieved with the code:

    98   amounts of trace output. This redirection can be achieved with the code:

    99 *}

    99 *}

   426   "get_thm_names_from_ss @{simpset}" 

   426   "get_thm_names_from_ss @{simpset}" 

   427   "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}

   427   "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}

   428 

   428 

   429   Again, this way or referencing simpsets makes you independent from additions

   429   Again, this way or referencing simpsets makes you independent from additions

   430   of lemmas to the simpset by the user that potentially cause loops.

   430   of lemmas to the simpset by the user that potentially cause loops.

   437 

   431 

   438   While antiquotations have many applications, they were originally introduced in order 

   432   While antiquotations have many applications, they were originally introduced in order 

   439   to avoid explicit bindings for theorems such as:

   433   to avoid explicit bindings for theorems such as:

   440 *}

   434 *}

   441 

   435 

   723 

   717 

   724   The difference between both functions is that @{ML extern_const in Sign} returns

   718   The difference between both functions is that @{ML extern_const in Sign} returns

   725   the smallest name that is still unique, whereas @{ML base_name in Sign} always

   719   the smallest name that is still unique, whereas @{ML base_name in Sign} always

   726   strips off all qualifiers.

   720   strips off all qualifiers.

   727 

   721 

   728   \begin{readmore}

   724   \begin{readmore}

   730   \end{readmore}

   726   \end{readmore}

   731 *}

   727 *}

   732 

   728 

   733 

   729 

   734 section {* Type-Checking *}

   730 section {* Type-Checking *}

   769 in

   765 in

   770   cterm_of @{theory} 

   766   cterm_of @{theory} 

   771       (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)

   767       (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)

   772 end" "0 + 0"}

   768 end" "0 + 0"}

   773 

   769 

   774   \begin{exercise}

   783   \begin{exercise}

   775   Check that the function defined in Exercise~\ref{fun:revsum} returns a

   784   Check that the function defined in Exercise~\ref{fun:revsum} returns a

   776   result that type-checks.

   785   result that type-checks.

   777   \end{exercise}

   786   \end{exercise}

   778 

   787 

   828   Instead of giving explicitly the type for the constant @{text "plus"} and the free 

   837   Instead of giving explicitly the type for the constant @{text "plus"} and the free 

   829   variable @{text "x"}, the type-inference filles in the missing information.

   838   variable @{text "x"}, the type-inference filles in the missing information.

   830 

   839 

   831   \begin{readmore}

   840   \begin{readmore}

   832   See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,

   841   See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,

   834   \end{readmore}

   845   \end{readmore}

   835 *}

   846 *}

   836 

   847 

   837 

   848 

   838 section {* Theorems *}

   849 section {* Theorems *}

  1023   then you can see the lemma is added to the initially empty list.

  1034   then you can see the lemma is added to the initially empty list.

  1024 

  1035 

  1025   @{ML_response_fake [display,gray]

  1036   @{ML_response_fake [display,gray]

  1026   "!my_thms" "[\"True\"]"}

  1037   "!my_thms" "[\"True\"]"}

  1027 

  1038 

  1029 *}

  1040 *}

  1030 

  1041 

  1031 declare test[my_thms] trueI_2[my_thms add]

  1042 declare test[my_thms] trueI_2[my_thms add]

  1032 

  1043 

  1033 text {*

  1044 text {*