src/HOL/Nonstandard_Analysis/HyperDef.thy
changeset 63651 f8e79d14d61f
parent 63648 f9f3006a5579
child 64435 c93b0e6131c3