src/HOL/RealDef.thy
changeset 42082 47f8bfe0f597
parent 41920 d4fb7a418152
child 42112 9cb122742f5c
equal deleted inserted replaced
42081:21697a5cb34a 42082:47f8bfe0f597