# HG changeset patch
# User nipkow
# Date 1180868308 -7200
# Node ID 098a23702aba3797df0812a64362c3fb2926da9c
# Parent  4d8a0976fa1caf819f4fe77a50109ae96c158d31
*** empty log message ***

diff -r 4d8a0976fa1c -r 098a23702aba src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Jun 02 20:14:38 2007 +0200
+++ b/src/HOL/List.thy	Sun Jun 03 12:58:28 2007 +0200
@@ -221,10 +221,16 @@
 
 subsubsection {* List comprehehsion *}
 
-text{* At the moment this theory provides only the input syntax for
-list comprehension: @{text"[x. x \<leftarrow> xs, \<dots>]"} rather than
-\verb![x| x <- xs, ...]! as in Haskell.
-
+text{* Input syntax for Haskell-like list comprehension
+notation. Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"}, the list of all pairs of distinct elements from @{text xs} and @{text ys}.
+
+There are a number of differences to Haskell.  The general synatx is
+@{text"[e. p \<leftarrow> xs, \<dots>]"} rather than \verb![x| x <- xs, ...]!. The
+first qualifier must be a generator (@{text"p \<leftarrow> xs"}). Patterns in
+generators can only be tuples (at the moment). Finally, guards are
+translated into filters, which simplifies theorem proving.
+*}
+(*
 The print translation from internal form to list comprehensions would
 be nice. Unfortunately one cannot just turn the translations around
 because in the final equality @{text p} occurs twice on the
@@ -234,17 +240,18 @@
 support. For example, it would be nice if
 @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
 produced something like
-@{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.  *}
-
-nonterminals lc_gentest
+@{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
+*)
+
+nonterminals lc_qual
 
 syntax
-"_listcompr" :: "'a \<Rightarrow> idt \<Rightarrow> 'b list \<Rightarrow> lc_gentest \<Rightarrow> 'a list" ("[_ . _ \<leftarrow> __")
-"_listcompr" :: "'a \<Rightarrow> idt \<Rightarrow> 'b list \<Rightarrow> lc_gentest \<Rightarrow> 'a list" ("[_ . _ <- __")
-"_lc_end" :: "lc_gentest" ("]")
-"_lc_gen" :: "idt \<Rightarrow> 'a list \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",_ \<leftarrow> __")
-"_lc_gen" :: "idt \<Rightarrow> 'a list \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",_ <- __")
-"_lc_test" :: "bool \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",__")
+"_listcompr" :: "'a \<Rightarrow> pttrn \<Rightarrow> 'b list \<Rightarrow> lc_qual \<Rightarrow> 'a list"  ("[_ . _ \<leftarrow> __")
+"_listcompr" :: "'a \<Rightarrow> pttrn \<Rightarrow> 'b list \<Rightarrow> lc_qual \<Rightarrow> 'a list"  ("[_ . _ <- __")
+"_lc_end" :: "lc_qual" ("]")
+"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual \<Rightarrow> lc_qual" (",_ \<leftarrow> __")
+"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual \<Rightarrow> lc_qual" (",_ <- __")
+"_lc_test" :: "bool \<Rightarrow> lc_qual \<Rightarrow> lc_qual" (",__")
 
 
 translations