src/HOL/Tools/reflection.ML
changeset 73839 0638fa8c01bc
parent 69593 3dda49e08b9d
child 74561 8e6c973003c8
equal deleted inserted replaced
73838:0e6a5a6cc767 73839:0638fa8c01bc