src/HOL/NSA/Hypercomplex.thy
changeset 47840 732ea1f08e3f
parent 27468 0783dd1dc13d