src/HOL/NSA/Hypercomplex.thy
changeset 27475 61b979a2c820
parent 27468 0783dd1dc13d