list syntax details
authornipkow
Sun Jun 03 19:06:56 2018 +0200 (13 months ago)
changeset 683645c579bb9adb1
parent 68363 23b2fad1729a
child 68365 f9379279f98c
child 68386 98cf1c823c48
list syntax details
NEWS
src/Doc/Main/Main_Doc.thy
src/Doc/Main/document/root.tex
     1.1 --- a/NEWS	Sun Jun 03 18:23:38 2018 +0200
     1.2 +++ b/NEWS	Sun Jun 03 19:06:56 2018 +0200
     1.3 @@ -315,8 +315,10 @@
     1.4  * Theory List: functions "sorted_wrt" and "sorted" now compare every
     1.5    element in a list to all following elements, not just the next one.
     1.6  
     1.7 -* Theory List: the non-standard filter-syntax "[x <- xs. P]" is
     1.8 -  deprecated and is currently only available as input syntax anymore.
     1.9 +* Theory List: Synatx:
    1.10 +  - filter-syntax "[x <- xs. P]" is no longer output syntax
    1.11 +    but only input syntax.
    1.12 +  - list comprehension syntax now supports tuple patterns in "pat <- xs".
    1.13  
    1.14  * Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
    1.15  
     2.1 --- a/src/Doc/Main/Main_Doc.thy	Sun Jun 03 18:23:38 2018 +0200
     2.2 +++ b/src/Doc/Main/Main_Doc.thy	Sun Jun 03 19:06:56 2018 +0200
     2.3 @@ -571,13 +571,15 @@
     2.4  \<open>[x\<^sub>1,\<dots>,x\<^sub>n]\<close> & \<open>x\<^sub>1 # \<dots> # x\<^sub>n # []\<close>\\
     2.5  @{term"[m..<n]"} & @{term[source]"upt m n"}\\
     2.6  @{term"[i..j]"} & @{term[source]"upto i j"}\\
     2.7 -\<open>[e. x \<leftarrow> xs]\<close> & @{term"map (%x. e) xs"}\\
     2.8  @{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\
     2.9  @{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\
    2.10  \end{supertabular}
    2.11  \<^medskip>
    2.12  
    2.13 -List comprehension: \<open>[e. q\<^sub>1, \<dots>, q\<^sub>n]\<close> where each
    2.14 +Filter input syntax \<open>[pat \<leftarrow> e. b]\<close>, where
    2.15 +\<open>pat\<close> is a tuple pattern, which stands for @{term "filter (\<lambda>pat. b) e"}.
    2.16 +
    2.17 +List comprehension input syntax: \<open>[e. q\<^sub>1, \<dots>, q\<^sub>n]\<close> where each
    2.18  qualifier \<open>q\<^sub>i\<close> is either a generator \mbox{\<open>pat \<leftarrow> e\<close>} or a
    2.19  guard, i.e.\ boolean expression.
    2.20  
     3.1 --- a/src/Doc/Main/document/root.tex	Sun Jun 03 18:23:38 2018 +0200
     3.2 +++ b/src/Doc/Main/document/root.tex	Sun Jun 03 19:06:56 2018 +0200
     3.3 @@ -2,13 +2,14 @@
     3.4  \usepackage{lmodern}
     3.5  \usepackage[T1]{fontenc}
     3.6  
     3.7 -\oddsidemargin=4.6mm
     3.8 -\evensidemargin=4.6mm
     3.9 -\textwidth=150mm
    3.10 -\topmargin=4.6mm
    3.11 -\headheight=0mm
    3.12 -\headsep=0mm
    3.13 -\textheight=234mm
    3.14 +%shortens document but can cause odd page breaks
    3.15 +%\oddsidemargin=4.6mm
    3.16 +%\evensidemargin=4.6mm
    3.17 +%\textwidth=150mm
    3.18 +%\topmargin=4.6mm
    3.19 +%\headheight=0mm
    3.20 +%\headsep=0mm
    3.21 +%\textheight=234mm
    3.22  
    3.23  \usepackage{isabelle,isabellesym}
    3.24  \usepackage{amssymb}