equal
deleted
inserted
replaced
547 instead of "arbitrary" |
547 instead of "arbitrary" |
548 |
548 |
549 * new constant "undefined" with axiom "undefined x = undefined" |
549 * new constant "undefined" with axiom "undefined x = undefined" |
550 |
550 |
551 * new class "default" with associated constant "default" |
551 * new class "default" with associated constant "default" |
|
552 |
|
553 * new function listsum :: 'a list => 'a for arbitrary monoids. |
|
554 Special syntax: "SUM x <- xs. f x" (and latex variants) |
552 |
555 |
553 * Library/List_Comprehension.thy provides Haskell-like input syntax for list |
556 * Library/List_Comprehension.thy provides Haskell-like input syntax for list |
554 comprehensions. |
557 comprehensions. |
555 |
558 |
556 * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals |
559 * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals |