src/HOL/NSA/Hypercomplex.thy
changeset 28830 261bf00c6ede
parent 27468 0783dd1dc13d
equal deleted inserted replaced
28829:c67ab5df760b 28830:261bf00c6ede