src/HOL/Complex/NSComplexArith.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Complex/NSComplexArith.thy	Tue Dec 23 18:26:03 2003 +0100
@@ -0,0 +1,19 @@
+(*  Title:       NSComplexArith
+    Author:      Lawrence C. Paulson
+    Copyright:   2003  University of Cambridge
+
+Common factor cancellation
+*)
+
+theory NSComplexArith = NSComplexBin
+files "hcomplex_arith.ML":
+
+subsubsection{*Division By @{term "-1"}*}
+
+lemma hcomplex_divide_minus1 [simp]: "x/-1 = -(x::hcomplex)"
+by simp
+
+lemma hcomplex_minus1_divide [simp]: "-1/(x::hcomplex) = - (1/x)"
+by (simp add: hcomplex_divide_def hcomplex_minus_inverse)
+
+end