src/HOL/Nonstandard_Analysis/HyperDef.thy
changeset 70568 6e055d313f73
parent 70356 4a327c061870
child 70723 4e39d87c9737