src/HOL/ex/Term_Of_Syntax.thy
changeset 29156 89f76a58a378
parent 28965 1de908189869
child 31139 0b615ac7eeaf