src/HOL/Real.thy
changeset 57229 489083abce44
parent 56889 48a745e1bde7
child 57275 0ddb5b755cdc