isabelle: src/HOL/Algebra/abstract/PID.thy@cc8e4276d093 (annotated)

7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	1	(*
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	2	Principle ideal domains
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	3	Author: Clemens Ballarin, started 5 October 1999
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	4	*)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	5
20318 0e0ea63fe768 Restructured algebra library, added ideals and quotient rings. ballarin parents: 17479 diff changeset	6	theory PID imports Ideal2 begin
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	7
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 7998 diff changeset	8	instance pid < factorial
68a7acb5f22e converted to Isar theory format; wenzelm parents: 7998 diff changeset	9	apply intro_classes
68a7acb5f22e converted to Isar theory format; wenzelm parents: 7998 diff changeset	10	apply (erule pid_irred_imp_prime)
68a7acb5f22e converted to Isar theory format; wenzelm parents: 7998 diff changeset	11	done
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	12
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	13	end

author	wenzelm
	Mon, 01 Mar 2010 17:12:43 +0100
changeset 35414	cc8e4276d093
parent 29665	2b956243d123
child 35849	b5522b51cb1e
permissions	-rw-r--r--