# HG changeset patch
# User huffman
# Date 1313618537 25200
# Node ID 7784fa3232cec5fa086a8f64bdf48d60d30d7a87
# Parent  b922e91dd1d9c632550ad46437fc754cbe7b74e5
Determinants.thy: avoid using mem_def/Collect_def

diff -r b922e91dd1d9 -r 7784fa3232ce src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Wed Aug 17 14:42:59 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Wed Aug 17 15:02:17 2011 -0700
@@ -131,7 +131,7 @@
   {fix p assume p: "p \<in> {p. p permutes ?U}"
     from p have pU: "p permutes ?U" by blast
     have sth: "sign (inv p) = sign p"
-      by (metis sign_inverse fU p mem_def Collect_def permutation_permutes)
+      by (metis sign_inverse fU p mem_Collect_eq permutation_permutes)
     from permutes_inj[OF pU]
     have pi: "inj_on p ?U" by (blast intro: subset_inj_on)
     from permutes_image[OF pU]