src/HOL/Bali/Name.thy
changeset 25577 d739f48ef40c
parent 24783 5a3e336a2e37
child 32960 69916a850301
equal deleted inserted replaced
25576:ee11881606b7 25577:d739f48ef40c