src/HOL/ex/Term_Of_Syntax.thy
changeset 28262 aa7ca36d67fd
parent 28258 4bf450d50c32
child 28335 25326092cf9a