src/HOL/ex/Term_Of_Syntax.thy
changeset 30254 7b8afdfa2f83
parent 28965 1de908189869
child 31139 0b615ac7eeaf