changeset 35849 | b5522b51cb1e |
parent 29665 | 2b956243d123 |
--- a/src/HOL/Algebra/abstract/PID.thy Sun Mar 21 16:51:37 2010 +0100 +++ b/src/HOL/Algebra/abstract/PID.thy Sun Mar 21 17:12:31 2010 +0100 @@ -1,9 +1,11 @@ -(* - Principle ideal domains - Author: Clemens Ballarin, started 5 October 1999 +(* Author: Clemens Ballarin, started 5 October 1999 + +Principle ideal domains. *) -theory PID imports Ideal2 begin +theory PID +imports Ideal2 +begin instance pid < factorial apply intro_classes