src/Tools/induct.ML
changeset 82456 690a018f7370
parent 81954 6f2bcdfa9a19
child 82587 7415414bd9d8