| changeset 55416 | dd7992d4a61a |
| parent 54459 | f43ae1afd08a |
| child 56643 | 41d3596d8a64 |
--- a/src/HOL/Library/IArray.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Library/IArray.thy Wed Feb 12 08:35:57 2014 +0100 @@ -63,11 +63,11 @@ by (cases as) simp lemma [code]: -"iarray_rec f as = f (IArray.list_of as)" +"rec_iarray f as = f (IArray.list_of as)" by (cases as) simp lemma [code]: -"iarray_case f as = f (IArray.list_of as)" +"case_iarray f as = f (IArray.list_of as)" by (cases as) simp lemma [code]: