src/HOL/Library/Extended_Real.thy
changeset 48102 9ed089bcad93
parent 47108 2a1953f0d20d
child 50104 de19856feb54
equal deleted inserted replaced
48101:1b9796b7ab03 48102:9ed089bcad93