ProgTutorial/Intro.thy
changeset 569 f875a25aa72d
parent 568 be23597e81db
child 574 034150db9d91
equal deleted inserted replaced
568:be23597e81db 569:f875a25aa72d
   150   simple ML-expression:
   150   simple ML-expression:
   151 
   151 
   152   \begin{isabelle}
   152   \begin{isabelle}
   153   \begin{graybox}
   153   \begin{graybox}
   154   \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline
   154   \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline
   155   \hspace{5mm}@{ML "3 + 4"}\isanewline
   155   \hspace{5mm}@{ML \<open>3 + 4\<close>}\isanewline
   156   \<open>\<verbclose>\<close>
   156   \<open>\<verbclose>\<close>
   157   \end{graybox}
   157   \end{graybox}
   158   \end{isabelle}
   158   \end{isabelle}
   159   
   159   
   160   These boxes correspond to how code can be processed inside the interactive
   160   These boxes correspond to how code can be processed inside the interactive
   161   environment of Isabelle. It is therefore easy to experiment with the code
   161   environment of Isabelle. It is therefore easy to experiment with the code
   162   that is shown in this tutorial. However, for better readability we will drop
   162   that is shown in this tutorial. However, for better readability we will drop
   163   the enclosing \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> and just
   163   the enclosing \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> and just
   164   write:
   164   write:
   165 
   165 
   166   @{ML [display,gray] "3 + 4"}
   166   @{ML [display,gray] \<open>3 + 4\<close>}
   167   
   167   
   168   Whenever appropriate we also show the response the code 
   168   Whenever appropriate we also show the response the code 
   169   generates when evaluated. This response is prefixed with a 
   169   generates when evaluated. This response is prefixed with a 
   170   @{text [quotes] ">"}, like:
   170   @{text [quotes] ">"}, like:
   171 
   171 
   172   @{ML_matchresult [display,gray] "3 + 4" "7"}
   172   @{ML_matchresult [display,gray] \<open>3 + 4\<close> \<open>7\<close>}
   173 
   173 
   174   The user-level commands of Isabelle (i.e., the non-ML code) are written
   174   The user-level commands of Isabelle (i.e., the non-ML code) are written
   175   in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},
   175   in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},
   176   \isacommand{foobar} and so on).  We use \<open>$ \<dots>\<close> to indicate that a
   176   \isacommand{foobar} and so on).  We use \<open>$ \<dots>\<close> to indicate that a
   177   command needs to be run in a UNIX-shell, for example:
   177   command needs to be run in a UNIX-shell, for example: