src/HOL/Lambda/InductTermi.thy
changeset 11364 01020b10c0a7
parent 9941 fe05af7ec816
child 11639 4213422388c4