src/HOL/Algebra/abstract/Factor.thy
changeset 17479 68a7acb5f22e
parent 13735 7de9342aca7a
child 20318 0e0ea63fe768
     1.1 --- a/src/HOL/Algebra/abstract/Factor.thy	Sat Sep 17 20:16:35 2005 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/Factor.thy	Sat Sep 17 20:49:14 2005 +0200
     1.3 @@ -4,15 +4,13 @@
     1.4      Author: Clemens Ballarin, started 25 November 1997
     1.5  *)
     1.6  
     1.7 -Factor = Ring +
     1.8 +theory Factor imports Ring begin
     1.9  
    1.10 -consts
    1.11 -  Factorisation	:: ['a::ring, 'a list, 'a] => bool
    1.12 +constdefs
    1.13 +  Factorisation :: "['a::ring, 'a list, 'a] => bool"
    1.14    (* factorisation of x into a list of irred factors and a unit u *)
    1.15 -
    1.16 -defs
    1.17 -  Factorisation_def	"Factorisation x factors u == 
    1.18 -                           x = foldr op* factors u &
    1.19 -                           (ALL a : set factors. irred a) & u dvd 1"
    1.20 +  "Factorisation x factors u ==
    1.21 +     x = foldr op* factors u &
    1.22 +     (ALL a : set factors. irred a) & u dvd 1"
    1.23  
    1.24  end