src/HOL/Algebra/abstract/PID.thy
changeset 7998 3d0c34795831
child 17479 68a7acb5f22e
equal deleted inserted replaced
7997:a1fb91eb9b4d 7998:3d0c34795831
       
     1 (*
       
     2     Principle ideal domains
       
     3     $Id$
       
     4     Author: Clemens Ballarin, started 5 October 1999
       
     5 *)
       
     6 
       
     7 PID = Ideal +
       
     8 
       
     9 instance
       
    10   pid < factorial	(TrueI, pid_irred_imp_prime)
       
    11 
       
    12 end
       
    13