equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 Factor = Ring + |
7 Factor = Ring + |
8 |
8 |
9 consts |
9 consts |
10 Factorisation :: ['a::ringS, 'a list, 'a] => bool |
10 Factorisation :: ['a::ring, 'a list, 'a] => bool |
11 (* factorisation of x into a list of irred factors and a unit u *) |
11 (* factorisation of x into a list of irred factors and a unit u *) |
12 |
12 |
13 defs |
13 defs |
14 Factorisation_def "Factorisation x factors u == |
14 Factorisation_def "Factorisation x factors u == |
15 x = foldr op* factors u & |
15 x = foldr op* factors u & |
16 (ALL a : set factors. irred a) & u dvd <1>" |
16 (ALL a : set factors. irred a) & u dvd 1" |
17 |
17 |
18 end |
18 end |