| 2013-11-16 | nipkow | 2013-11-16 | added functions all and exists to IArray | file | diff | annotate |
| 2013-02-15 | haftmann | 2013-02-15 | two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one | file | diff | annotate |
| 2013-02-13 | haftmann | 2013-02-13 | IArray ignorant of particular representation of nat | file | diff | annotate |
| 2012-11-21 | nipkow | 2012-11-21 | new theory of immutable arrays | file | diff | annotate |