# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1275161408 -7200
# Node ID c2dde8c7174f52251f48ee2185584814b98e848a
# Parent  94538ddcac9b3920b1b18822eaa2ad27417e241a
tuned

diff -r 94538ddcac9b -r c2dde8c7174f ProgTutorial/Recipes/CallML.thy
--- a/ProgTutorial/Recipes/CallML.thy	Sat May 29 12:30:02 2010 +0200
+++ b/ProgTutorial/Recipes/CallML.thy	Sat May 29 21:30:08 2010 +0200
@@ -23,7 +23,7 @@
   certificate, that for primality, although it, too, can be treated in the
   same manner. 
 
-  The example we looking at here is an ML function for finding a factor 
+  The example we are looking at here is an ML function for finding a factor 
   of a number. We first declare its type:
 *}
 
@@ -36,9 +36,8 @@
 *}
 
 lemma factor_non_prime:
-  assumes "let k = factor n in k \<noteq> 1 \<and> k \<noteq> n \<and> k dvd n"
-  shows "\<not> prime n"
-using assms by(auto simp: prime_nat_def Let_def)
+  "let k = factor n in k \<noteq> 1 \<and> k \<noteq> n \<and> k dvd n \<Longrightarrow> \<not> prime n"
+  by (auto simp: prime_nat_def Let_def)
 
 text{* 
   Note that the premise is executable once we have defined 
@@ -81,7 +80,7 @@
   done
 
 text{* 
-  Note, hawever, the command \isacommand{code\_const} cannot check that the ML function
+  Note, however, the command \isacommand{code\_const} cannot check that the ML function
   has the required type. Therefore in the worst case a type mismatch will be detected by
   the ML-compiler when we try to evaluate an expression involving @{const
   factor}. It could also happen that @{const factor} is (accidentally)
@@ -91,7 +90,8 @@
   definitions can lead to compile time or run time exceptions, or to failed
   proofs.
 
-  The above example was easy because we forced Iabelle (via the inclusion of @{theory
+  The above example was easy because we forced Isabelle (via the inclusion of the
+  theory @{theory
   Efficient_Nat}) to implement @{typ nat} by @{text int}, a predefined 
   ML-type.  By default, Isabelle implements, for example, the HOL-type 
   @{text list} by the corresponding ML-type. Thus the following variation 
@@ -109,7 +109,7 @@
   gives its implementation in ML; the third makes it executable 
   in HOL, and the last is just a test.  In this way, you can easily 
   interface with ML-functions whose types involve 
-  @{text bool}, @{text int}, @{text list}, @{text option} and @{text pairs}, 
+  @{text bool}, @{text int}, @{text list}, @{text option} and pairs, 
   only. If you have arbitrary tuples, for example, then you have to code 
   them as nested pairs.
 
diff -r 94538ddcac9b -r c2dde8c7174f progtutorial.pdf
Binary file progtutorial.pdf has changed