# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1239227259 -3600
# Node ID dc955603d81335a51422b8cf721d39f1334f8b49
# Parent  f84bc59cb5be23a3106378a233a8ef4fff0cac1c
explained uses and use commands

diff -r f84bc59cb5be -r dc955603d813 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Wed Apr 08 13:42:18 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Wed Apr 08 22:47:39 2009 +0100
@@ -57,8 +57,24 @@
   code, rather they indicate what the response is when the code is evaluated.
 
   Once a portion of code is relatively stable, you usually want to export it
-  to a separate ML-file. Such files can then be included in a theory by using
-  the \isacommand{uses}-command in the header of the theory, like:
+  to a separate ML-file. Such files can then be included somewhere inside a 
+  theory by using the command \isacommand{use}. For example
+
+  \begin{center}
+  \begin{tabular}{@ {}l}
+  \isacommand{theory} FirstSteps\\
+  \isacommand{imports} Main\\
+  \isacommand{uses}~@{text "(\"file_to_be_included.ML\")"} @{text "\<dots>"}\\
+  \isacommand{begin}\\
+  \ldots\\
+  \isacommand{use}~@{text "\"file_to_be_included.ML\""}\\
+  \ldots
+  \end{tabular}
+  \end{center}
+
+  The \isacommand{uses}-command in the header of the theory is needed in order 
+  to indicate the dependency of the theory on the ML-file. Alternatively, the 
+  file can be included by just writing in the header
 
   \begin{center}
   \begin{tabular}{@ {}l}
@@ -69,7 +85,8 @@
   \ldots
   \end{tabular}
   \end{center}
-  
+
+  Note that no parentheses are given this time.
 *}
 
 section {* Debugging and Printing\label{sec:printing} *}
@@ -227,6 +244,8 @@
 section {* Combinators\label{sec:combinators} *}
 
 text {*
+  (FIXME: Calling convention)
+
   For beginners perhaps the most puzzling parts in the existing code of Isabelle are
   the combinators. At first they seem to greatly obstruct the
   comprehension of the code, but after getting familiar with them, they
@@ -1554,6 +1573,7 @@
   valid local theory.
 *}
 
+(*
 ML{*signature UNIVERSAL_TYPE =
 sig
   type t
@@ -1616,6 +1636,10 @@
 
 ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*}
 
+ML {* LocalTheory.restore *}
+ML {* LocalTheory.set_group *}
+*)
+
 section {* Storing Theorems\label{sec:storing} (TBD) *}
 
 text {* @{ML PureThy.add_thms_dynamic} *}
diff -r f84bc59cb5be -r dc955603d813 ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Wed Apr 08 13:42:18 2009 +0100
+++ b/ProgTutorial/Intro.thy	Wed Apr 08 22:47:39 2009 +0100
@@ -10,12 +10,12 @@
   Isabelle programming, and also explain tricks of the trade. The best way to
   get to know the ML-level of Isabelle is by experimenting with the many code
   examples included in the tutorial. The code is as far as possible checked
-  against recent versions of Isabelle. If something does not work, then please
-  let us know. It is impossible for us to know every environment, operating
-  system or editor in which Isabelle is used. If you have comments, criticism
-  or like to add to the tutorial, please feel free---you are most welcome! The
-  tutorial is meant to be gentle and comprehensive. To achieve this we need
-  your feedback.
+  against \input{version}. If something does not work, 
+  then please let us know. It is impossible for us to know every environment, 
+  operating system or editor in which Isabelle is used. If you have comments, 
+  criticism or like to add to the tutorial, please feel free---you are most 
+  welcome! The tutorial is meant to be gentle and comprehensive. To achieve 
+  this we need your feedback.
 *}
 
 section {* Intended Audience and Prior Knowledge *}
@@ -60,9 +60,9 @@
   things really work. Therefore you should not hesitate to look at the
   way things are actually implemented. More importantly, it is often
   good to look at code that does similar things as you want to do and
-  learn from it. The GNU/UNIX command @{text "grep -R"} is
+  learn from it. The GNU/UNIX command \mbox{@{text "grep -R"}} is
   often your best friend while programming with Isabelle, or
-  hypersearch if you use jEdit under MacOSX.
+  hypersearch if you program using jEdit under MacOSX.
   \end{description}
 
 *}
@@ -136,6 +136,7 @@
   \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context}
   \item @{text lthy} for local theories; ML-type: @{ML_type local_theory}
   \item @{text context} for generic contexts; ML-type @{ML_type Context.generic}
+  \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix}
   \end{itemize}
 *}
 
diff -r f84bc59cb5be -r dc955603d813 progtutorial.pdf
Binary file progtutorial.pdf has changed