author | ballarin |
Thu, 03 Aug 2006 14:57:26 +0200 | |
changeset 20318 | 0e0ea63fe768 |
parent 17479 | 68a7acb5f22e |
child 21423 | 6cdd0589aa73 |
permissions | -rw-r--r-- |
(* Factorisation within a factorial domain $Id$ Author: Clemens Ballarin, started 25 November 1997 *) theory Factor imports Ring2 begin constdefs Factorisation :: "['a::ring, 'a list, 'a] => bool" (* factorisation of x into a list of irred factors and a unit u *) "Factorisation x factors u == x = foldr op* factors u & (ALL a : set factors. irred a) & u dvd 1" end