src/HOL/Induct/ABexp.thy
changeset 44862 fe711df09fd9
parent 39246 9e58f0499f57
child 46914 c2ca2c3d23a6