src/HOL/Complex.thy
changeset 62102 877463945ce9
parent 62101 26c0a70f78a3
child 62379 340738057c8c
--- a/src/HOL/Complex.thy	Fri Jan 08 17:40:59 2016 +0100
+++ b/src/HOL/Complex.thy	Fri Jan 08 17:41:04 2016 +0100
@@ -284,6 +284,8 @@
 
 end
 
+declare uniformity_Abort[where 'a=complex, code]
+
 lemma norm_ii [simp]: "norm ii = 1"
   by (simp add: norm_complex_def)