src/HOL/Nonstandard_Analysis/Hypercomplex.thy
changeset 62825 e6e80a8bf624
parent 62479 716336f19aa9