isabelle: src/HOL/Complex/ComplexBin.thy@717b1eb434f1 (annotated)

13957 10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	1	(* Title: ComplexBin.thy
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	2	Author: Jacques D. Fleuriot
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	3	Copyright: 2001 University of Edinburgh
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	4	Descrition: Binary arithmetic for the complex numbers
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	5	This case is reduced to that for the reals.
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	6	*)
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	7
15131 c69542757a4d New theory header syntax. nipkow parents: 14387 diff changeset	8	theory ComplexBin
15140 322485b816ac import -> imports nipkow parents: 15131 diff changeset	9	imports Complex
15131 c69542757a4d New theory header syntax. nipkow parents: 14387 diff changeset	10	begin
13957 10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	11
15131 c69542757a4d New theory header syntax. nipkow parents: 14387 diff changeset	12	end
c69542757a4d New theory header syntax. nipkow parents: 14387 diff changeset	13