equal
deleted
inserted
replaced
128 |
128 |
129 \index{*list (type)}% |
129 \index{*list (type)}% |
130 Lists are one of the essential datatypes in computing. We expect that you |
130 Lists are one of the essential datatypes in computing. We expect that you |
131 are already familiar with their basic operations. |
131 are already familiar with their basic operations. |
132 Theory \isa{ToyList} is only a small fragment of HOL's predefined theory |
132 Theory \isa{ToyList} is only a small fragment of HOL's predefined theory |
133 \thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}. |
133 \thydx{List}\footnote{\url{https://isabelle.in.tum.de/library/HOL/List.html}}. |
134 The latter contains many further operations. For example, the functions |
134 The latter contains many further operations. For example, the functions |
135 \cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first |
135 \cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first |
136 element and the remainder of a list. (However, pattern matching is usually |
136 element and the remainder of a list. (However, pattern matching is usually |
137 preferable to \isa{hd} and \isa{tl}.) |
137 preferable to \isa{hd} and \isa{tl}.) |
138 Also available are higher-order functions like \isa{map} and \isa{filter}. |
138 Also available are higher-order functions like \isa{map} and \isa{filter}. |