| changeset 30949 | 37f887b55e7f |
| parent 30242 | aea5d7fa7ef5 |
| child 30952 | 7ab2716dd93b |
--- a/src/HOL/List.thy Fri Apr 17 15:14:06 2009 +0200 +++ b/src/HOL/List.thy Fri Apr 17 15:57:26 2009 +0200 @@ -198,7 +198,7 @@ definition rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where - "rotate n = rotate1 ^ n" + "rotate n = rotate1 ^^ n" definition list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where