src/HOL/Nonstandard_Analysis/StarDef.thy
changeset 63145 703edebd1d92
parent 62479 716336f19aa9
child 63456 3365c8ec67bd