# HG changeset patch
# User nipkow
# Date 1528045616 -7200
# Node ID 5c579bb9adb11cf7ad098f09bf26cfa71aacbead
# Parent  23b2fad1729a35b85fd2d01f769a8780202d5bb5
list syntax details

diff -r 23b2fad1729a -r 5c579bb9adb1 NEWS
--- a/NEWS	Sun Jun 03 18:23:38 2018 +0200
+++ b/NEWS	Sun Jun 03 19:06:56 2018 +0200
@@ -315,8 +315,10 @@
 * Theory List: functions "sorted_wrt" and "sorted" now compare every
   element in a list to all following elements, not just the next one.
 
-* Theory List: the non-standard filter-syntax "[x <- xs. P]" is
-  deprecated and is currently only available as input syntax anymore.
+* Theory List: Synatx:
+  - filter-syntax "[x <- xs. P]" is no longer output syntax
+    but only input syntax.
+  - list comprehension syntax now supports tuple patterns in "pat <- xs".
 
 * Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
 
diff -r 23b2fad1729a -r 5c579bb9adb1 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Sun Jun 03 18:23:38 2018 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Sun Jun 03 19:06:56 2018 +0200
@@ -571,13 +571,15 @@
 \<open>[x\<^sub>1,\<dots>,x\<^sub>n]\<close> & \<open>x\<^sub>1 # \<dots> # x\<^sub>n # []\<close>\\
 @{term"[m..<n]"} & @{term[source]"upt m n"}\\
 @{term"[i..j]"} & @{term[source]"upto i j"}\\
-\<open>[e. x \<leftarrow> xs]\<close> & @{term"map (%x. e) xs"}\\
 @{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\
 @{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\
 \end{supertabular}
 \<^medskip>
 
-List comprehension: \<open>[e. q\<^sub>1, \<dots>, q\<^sub>n]\<close> where each
+Filter input syntax \<open>[pat \<leftarrow> e. b]\<close>, where
+\<open>pat\<close> is a tuple pattern, which stands for @{term "filter (\<lambda>pat. b) e"}.
+
+List comprehension input syntax: \<open>[e. q\<^sub>1, \<dots>, q\<^sub>n]\<close> where each
 qualifier \<open>q\<^sub>i\<close> is either a generator \mbox{\<open>pat \<leftarrow> e\<close>} or a
 guard, i.e.\ boolean expression.
 
diff -r 23b2fad1729a -r 5c579bb9adb1 src/Doc/Main/document/root.tex
--- a/src/Doc/Main/document/root.tex	Sun Jun 03 18:23:38 2018 +0200
+++ b/src/Doc/Main/document/root.tex	Sun Jun 03 19:06:56 2018 +0200
@@ -2,13 +2,14 @@
 \usepackage{lmodern}
 \usepackage[T1]{fontenc}
 
-\oddsidemargin=4.6mm
-\evensidemargin=4.6mm
-\textwidth=150mm
-\topmargin=4.6mm
-\headheight=0mm
-\headsep=0mm
-\textheight=234mm
+%shortens document but can cause odd page breaks
+%\oddsidemargin=4.6mm
+%\evensidemargin=4.6mm
+%\textwidth=150mm
+%\topmargin=4.6mm
+%\headheight=0mm
+%\headsep=0mm
+%\textheight=234mm
 
 \usepackage{isabelle,isabellesym}
 \usepackage{amssymb}