src/HOL/RealDef.thy
changeset 50372 11c96cac860d
parent 49962 a8cc904a6820
child 51126 df86080de4cb
equal deleted inserted replaced
50371:9b6f5f758c31 50372:11c96cac860d