# HG changeset patch
# User schropp <schropp@in.tum.de>
# Date 1275338611 -7200
# Node ID 73437f42c9d3a4bef1be01d8c7f549702f6ec99e
# Parent  d04d1cd0e058d184d6c759115be9dd0991aea5e6
some more examples of ho-patterns

diff -r d04d1cd0e058 -r 73437f42c9d3 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Mon May 31 22:27:48 2010 +0200
+++ b/ProgTutorial/Essential.thy	Mon May 31 22:43:31 2010 +0200
@@ -983,13 +983,15 @@
   "let
   val trm_list = 
         [@{term_pat \"?X\"},              @{term_pat \"a\"},
-         @{term_pat \"\<lambda>a b. ?X a b\"},    @{term_pat \"\<lambda>a b. (op +) a b\"},
+         @{term_pat \"f (\<lambda>a b. ?X a b) c\"},
+         @{term_pat \"\<lambda>a b. (op +) a b\"},
          @{term_pat \"\<lambda>a. (op +) a ?Y\"}, @{term_pat \"?X ?Y\"},
-         @{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"}] 
+         @{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"},
+         @{term_pat \"?X a\"}] 
 in
   map Pattern.pattern trm_list
 end"
-  "[true, true, true, true, true, false, false, false]"}
+  "[true, true, true, true, true, false, false, false, false]"}
 
   The point of the restriction to patterns is that unification and matching 
   are decidable and produce most general unifiers, respectively matchers. 
diff -r d04d1cd0e058 -r 73437f42c9d3 progtutorial.pdf
Binary file progtutorial.pdf has changed