src/HOL/Inductive.thy
changeset 11295 66925f23ac7f
parent 11003 ee0838d89deb
child 11325 a5e0289dd56c