src/HOL/RealDef.thy
changeset 47259 2d4ea84278da
parent 47108 2a1953f0d20d
child 47428 45b58fec9024
equal deleted inserted replaced
47258:880e587eee9f 47259:2d4ea84278da