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