src/HOL/RealDef.thy
changeset 36634 f9b43d197d16
parent 36414 a19ba9bbc8dc
child 36776 c137ae7673d3