CookBook/Intro.thy
changeset 101 123401a5c8e9
parent 89 fee4942c4770
child 102 5e309df58557
equal deleted inserted replaced
100:dd8eebae11ec 101:123401a5c8e9
    91   generates when evaluated. This response is prefixed with a 
    91   generates when evaluated. This response is prefixed with a 
    92   @{text [quotes] ">"} like:
    92   @{text [quotes] ">"} like:
    93 
    93 
    94   @{ML_response [display,gray] "3 + 4" "7"}
    94   @{ML_response [display,gray] "3 + 4" "7"}
    95 
    95 
    96   The usual Isabelle commands are written in bold, for example \isacommand{lemma}, 
    96   The usual user-level commands of Isabelle are written in bold, for 
    97   \isacommand{foobar} and so on.  We use @{text "$"} to indicate that 
    97   example \isacommand{lemma}, \isacommand{foobar} and so on.  
    98   a command  needs to be run in the Unix-shell, for example
    98   We use @{text "$"} to indicate that a command  needs to be run 
       
    99   in the Unix-shell, for example
    99 
   100 
   100   @{text [display] "$ ls -la"}
   101   @{text [display] "$ ls -la"}
   101 
   102 
   102   Pointers to further information and Isabelle files are typeset in 
   103   Pointers to further information and Isabelle files are typeset in 
   103   italic and highlighted as follows:
   104   italic and highlighted as follows: