src/HOL/Library/Executable_Real.thy
changeset 23438 dd824e86fa8a
parent 23315 df3a7e9ebadb
child 24197 c9e3cb5e5681
equal deleted inserted replaced
23437:4a44fcc9dba9 23438:dd824e86fa8a