src/HOL/Import/HOL/HOL4Real.thy
changeset 18851 9502ce541f01
parent 17694 b7870c2bd7df
child 20485 3078fd2eec7b