src/HOL/Nonstandard_Analysis/Hypercomplex.thy
author wenzelm
Mon, 24 Oct 2022 20:37:32 +0200
changeset 76371 1ac2416e8432
parent 62479 716336f19aa9
permissions -rw-r--r--
tuned signature (again, amending f32ac01aef5e), e.g. relevant for Isabelle/DOF;

theory Hypercomplex
imports CLim Hyperreal
begin

end