| changeset 30661 | 54858c8ad226 |
| parent 30598 | eb827cd69fd3 |
| child 30837 | 3d4832d9f7e4 |
--- a/src/HOL/Library/Determinants.thy Mon Mar 23 08:14:22 2009 +0100 +++ b/src/HOL/Library/Determinants.thy Mon Mar 23 08:14:23 2009 +0100 @@ -5,7 +5,7 @@ header {* Traces, Determinant of square matrices and some properties *} theory Determinants - imports Euclidean_Space Permutations +imports Euclidean_Space Permutations begin subsection{* First some facts about products*}