src/HOL/ex/Term_Of_Syntax.thy
changeset 30242 aea5d7fa7ef5
parent 28965 1de908189869
child 31139 0b615ac7eeaf
equal deleted inserted replaced
30241:3a1aef73b2b2 30242:aea5d7fa7ef5