src/HOL/ex/Term_Of_Syntax.thy
changeset 30997 081e825c2218
parent 28965 1de908189869
child 31139 0b615ac7eeaf