equal
deleted
inserted
replaced
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 |
552 |
553 * Library/List_Comprehension provides Haskell-like input syntax for list |
553 * Library/List_Comprehension.thy provides Haskell-like input syntax for list |
554 comprehensions. |
554 comprehensions. |
555 |
555 |
556 * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals |
556 * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals |
557 when generating code. |
557 when generating code. |
558 |
558 |