src/HOL/Hyperreal/Hyperreal.thy
changeset 12915 2832fba717ec
parent 12224 02df7cbe7d25
child 13958 c1c67582c9b5
equal deleted inserted replaced
12914:71015f46b3c1 12915:2832fba717ec