src/HOL/Nonstandard_Analysis/Hypercomplex.thy
changeset 79272 899f37f6d218
parent 62479 716336f19aa9
equal deleted inserted replaced
79271:b14b289caaf6 79272:899f37f6d218