src/HOL/Hyperreal/ex/Sqrt_Script.thy
changeset 13049 ce180e5b7fa0
parent 13036 dca23533bdfb