# 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 @@ \[x\<^sub>1,\,x\<^sub>n]\ & \x\<^sub>1 # \ # x\<^sub>n # []\\\ @{term"[m..[e. x \ xs]\ & @{term"map (%x. e) xs"}\\ @{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\ @{term"\x\xs. e"} & @{term[source]"listsum (map (\x. e) xs)"}\\ \end{supertabular} \<^medskip> -List comprehension: \[e. q\<^sub>1, \, q\<^sub>n]\ where each +Filter input syntax \[pat \ e. b]\, where +\pat\ is a tuple pattern, which stands for @{term "filter (\pat. b) e"}. + +List comprehension input syntax: \[e. q\<^sub>1, \, q\<^sub>n]\ where each qualifier \q\<^sub>i\ is either a generator \mbox{\pat \ e\} 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}