src/HOL/Real.thy
changeset 67264 16f74b7c248a
parent 67226 ec32cdaab97b
child 67399 eab6ce8368fa
equal deleted inserted replaced
67263:449a989f42cd 67264:16f74b7c248a