equal
deleted
inserted
replaced
22 irred :: 'a::ringS => bool |
22 irred :: 'a::ringS => bool |
23 prime :: 'a::ringS => bool |
23 prime :: 'a::ringS => bool |
24 |
24 |
25 (* Fields *) |
25 (* Fields *) |
26 inverse :: 'a::ringS => 'a |
26 inverse :: 'a::ringS => 'a |
27 "'/'/" :: ['a, 'a] => 'a::ringS (infixl 70) |
27 "'/" :: ['a, 'a] => 'a::ringS (infixl 70) |
28 |
28 |
29 translations |
29 translations |
30 "a -- b" == "a + (-b)" |
30 "a -- b" == "a + (-b)" |
31 "a // b" == "a * inverse b" |
31 "a / b" == "a * inverse b" |
32 |
32 |
33 (* Class ring and ring axioms *) |
33 (* Class ring and ring axioms *) |
34 |
34 |
35 axclass |
35 axclass |
36 ring < ringS |
36 ring < ringS |