src/HOL/Tools/TFL/usyntax.ML
changeset 50444 f2241b8d0db5
parent 44121 44adaa6db327
child 55414 eab03e9cee8a
equal deleted inserted replaced
50443:b233d426fa0b 50444:f2241b8d0db5