3 begin

     3 begin

     4 

     4 

     5 chapter {* First Steps *}

     5 chapter {* First Steps *}

     6 

     6 

     7 text {*

     7 text {*

    10   in Isabelle is part of a theory. If you want to follow the code given in

     9   in Isabelle is part of a theory. If you want to follow the code given in

    11   this chapter, we assume you are working inside the theory starting with

    10   this chapter, we assume you are working inside the theory starting with

    12 

    11 

    13   \begin{center}

    12   \begin{center}

    14   \begin{tabular}{@ {}l}

    13   \begin{tabular}{@ {}l}

   888 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true

   887 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true

   889   | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true

   888   | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true

   890   | is_nil_or_all _ = false *}

   889   | is_nil_or_all _ = false *}

   891 

   890 

   892 text {*

   891 text {*

   893   Occasionally you have to calculate what the ``base'' name of a given

   898   Occasionally you have to calculate what the ``base'' name of a given

   894   constant is. For this you can use the function @{ML Sign.extern_const} or

   899   constant is. For this you can use the function @{ML Sign.extern_const} or

   895   @{ML Long_Name.base_name}. For example:

   900   @{ML Long_Name.base_name}. For example:

   896 

   901 

   897   @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}

   902   @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}