src/HOL/Real/Real.thy
changeset 6426 9a2ace82b68e
parent 5588 a3ab526bb891
child 7077 60b098bb8b8a
equal deleted inserted replaced
6425:9540aa1b5a9a 6426:9a2ace82b68e