src/HOL/Library/code_test.ML
changeset 64845 e5d4bc2016a6
parent 64582 3d20ded18f14
child 64901 18e6f83e4a09
equal deleted inserted replaced
64844:bb70dc05cd38 64845:e5d4bc2016a6