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

35849 b5522b51cb1e standard headers; wenzelm parents: 29665 diff changeset	1	(* Author: Clemens Ballarin, started 5 October 1999
b5522b51cb1e standard headers; wenzelm parents: 29665 diff changeset	2
b5522b51cb1e standard headers; wenzelm parents: 29665 diff changeset	3	Principle ideal domains.
7998 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
35849 b5522b51cb1e standard headers; wenzelm parents: 29665 diff changeset	6	theory PID
b5522b51cb1e standard headers; wenzelm parents: 29665 diff changeset	7	imports Ideal2
b5522b51cb1e standard headers; wenzelm parents: 29665 diff changeset	8	begin
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	9
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 7998 diff changeset	10	instance pid < factorial
68a7acb5f22e converted to Isar theory format; wenzelm parents: 7998 diff changeset	11	apply intro_classes
68a7acb5f22e converted to Isar theory format; wenzelm parents: 7998 diff changeset	12	apply (erule pid_irred_imp_prime)
68a7acb5f22e converted to Isar theory format; wenzelm parents: 7998 diff changeset	13	done
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	14
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	15	end

author	Cezary Kaliszyk <cezarykaliszyk@gmail.com>
	Wed, 04 Apr 2012 20:09:56 +0200
changeset 47363	c7fc95e722ff
parent 35849	b5522b51cb1e
permissions	-rw-r--r--