equal
deleted
inserted
replaced
11 |
11 |
12 Note that arrays cannot be printed directly but only by turning them into |
12 Note that arrays cannot be printed directly but only by turning them into |
13 lists first. Arrays could be converted back into lists for printing if they |
13 lists first. Arrays could be converted back into lists for printing if they |
14 were wrapped up in an additional constructor. *} |
14 were wrapped up in an additional constructor. *} |
15 |
15 |
16 datatype 'a iarray = IArray "'a list" |
16 datatype_new 'a iarray = IArray "'a list" |
17 |
17 |
18 primrec list_of :: "'a iarray \<Rightarrow> 'a list" where |
18 primrec list_of :: "'a iarray \<Rightarrow> 'a list" where |
19 "list_of (IArray xs) = xs" |
19 "list_of (IArray xs) = xs" |
20 hide_const (open) list_of |
20 hide_const (open) list_of |
21 |
21 |