Mercurial Mercurial > hg > isabelle-cookbook / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tunded
authorChristian Urban <urbanc@in.tum.de>
Wed, 02 Dec 2009 17:06:41 +0100
changeset 408 ef048892d0f0
parent 407 aee4abd02db1
child 409 f1743ce9dbf1
tunded
ProgTutorial/Advanced.thy file | annotate | diff | comparison | revisions
ProgTutorial/Essential.thy file | annotate | diff | comparison | revisions
ProgTutorial/Tactical.thy file | annotate | diff | comparison | revisions
progtutorial.pdf file | annotate | diff | comparison | revisions 
--- 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) *}
--- 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
--- 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.
Binary file progtutorial.pdf has changed
isabelle-cookbook