NEWS
changeset 23210 a0cb15114e7a
parent 23180 80b9caed2ba8
child 23251 471b576aad25
equal deleted inserted replaced
23209:098a23702aba 23210:a0cb15114e7a
   558 * new class "default" with associated constant "default"
   558 * new class "default" with associated constant "default"
   559 
   559 
   560 * new function listsum :: 'a list => 'a for arbitrary monoids.
   560 * new function listsum :: 'a list => 'a for arbitrary monoids.
   561   Special syntax: "SUM x <- xs. f x" (and latex variants)
   561   Special syntax: "SUM x <- xs. f x" (and latex variants)
   562 
   562 
   563 * Library/List_Comprehension.thy provides Haskell-like input syntax for list
   563 * new (input only) syntax for Haskell-like list comprehension, eg
   564   comprehensions.
   564   [(x,y). x <- xs, y <- ys, x ~= y]
       
   565   For details see List.thy.
   565 
   566 
   566 * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals
   567 * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals
   567     when generating code.
   568     when generating code.
   568 
   569 
   569 * Library/Pretty_Char.thy: maps HOL characters on target language character literals
   570 * Library/Pretty_Char.thy: maps HOL characters on target language character literals