# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259770001 -3600
# Node ID ef048892d0f0d696af406c1cb19629a0a343bee9
# Parent  aee4abd02db16c0eaef259ccd8733165b0fe11cb
tunded

diff -r aee4abd02db1 -r ef048892d0f0 ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Wed Dec 02 03:46:32 2009 +0100
+++ b/ProgTutorial/Advanced.thy	Wed Dec 02 17:06:41 2009 +0100
@@ -16,14 +16,14 @@
 text {*
   While terms, types and theorems are the most basic data structures in
   Isabelle, there are a number of layers built on top of them. Most of these
-  layers are concerned with storing and manipulating data. Handling
-  them properly is an essential skill for Isabelle programming. The most basic
-  layer are theories. They contain global data and can be seen as the
-  ``long-term memory'' of Isabelle. There is usually only one theory
-  active at each moment. Proof contexts and local theories, on the
+  layers are concerned with storing and manipulating data. Handling them
+  properly is an essential skill for programming on the ML-level of Isabelle
+  programming. The most basic layer are theories. They contain global data and
+  can be seen as the ``long-term memory'' of Isabelle. There is usually only
+  one theory active at each moment. Proof contexts and local theories, on the
   other hand, store local data for a task at hand. They act like the
-  ``short-term memory'' and there can be many of them that are active
-  in parallel. 
+  ``short-term memory'' and there can be many of them that are active in
+  parallel.
 *}
 
 section {* Theories\label{sec:theories} (TBD) *}
diff -r aee4abd02db1 -r ef048892d0f0 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Wed Dec 02 03:46:32 2009 +0100
+++ b/ProgTutorial/Essential.thy	Wed Dec 02 17:06:41 2009 +0100
@@ -1087,9 +1087,20 @@
 end"
 "NONE"}
 
-  In order to find a
-  reasonable solution for a unification problem, Isabelle also tries first to
-  solve the problem by higher-order pattern unification. 
+  In order to find a reasonable solution for a unification problem, Isabelle
+  also tries first to solve the problem by higher-order pattern
+  unification. Only in case of failure full higher-order unification is
+  called. This function has a built-in bound, which can be accessed and
+  manipulated as a configuration value:
+
+  @{ML_response_fake [display,gray]
+  "Config.get_thy @{theory} (Unify.search_bound_value)"
+  "Int 60"}
+
+  If this bound is reached during unification, Isabelle prints out the
+  warning message @{text [quotes] "Unification bound exceeded"} and
+  plenty of diagnostic information. 
+
 
   For higher-order matching the function is called @{ML_ind matchers in Unify}
   implemented in the structure @{ML_struct Unify}. Also this function returns
diff -r aee4abd02db1 -r ef048892d0f0 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Wed Dec 02 03:46:32 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Wed Dec 02 17:06:41 2009 +0100
@@ -2311,7 +2311,8 @@
 end*}
 
 text {*
-  The function @{ML bottom_conv in More_Conv} traverses first the the term and
+  If we regard terms as trees with variables and constants on the top, then 
+  @{ML bottom_conv in More_Conv} traverses first the the term and
   on the ``way down'' applies the conversion, whereas @{ML top_conv in
   More_Conv} applies the conversion on the ``way up''. To see the difference, 
   assume the following two meta-equations.
diff -r aee4abd02db1 -r ef048892d0f0 progtutorial.pdf
Binary file progtutorial.pdf has changed