author | ballarin |
Thu, 28 Nov 2002 10:50:42 +0100 | |
changeset 13735 | 7de9342aca7a |
parent 7998 | 3d0c34795831 |
child 17479 | 68a7acb5f22e |
permissions | -rw-r--r-- |
(* Factorisation within a factorial domain $Id$ Author: Clemens Ballarin, started 25 November 1997 *) Factor = Ring + consts Factorisation :: ['a::ring, 'a list, 'a] => bool (* factorisation of x into a list of irred factors and a unit u *) defs Factorisation_def "Factorisation x factors u == x = foldr op* factors u & (ALL a : set factors. irred a) & u dvd 1" end