src/HOL/Induct/Comb.thy
changeset 61087 1e36b5d021f2
parent 60530 44f9873d6f6f
child 61993 89206877f0ee