src/HOL/RealDef.thy
changeset 36302 4e7f5b22dd7d
parent 35635 90fffd5ff996
child 36349 39be26d1bc28
equal deleted inserted replaced
36301:72f4d079ebf8 36302:4e7f5b22dd7d