src/Tools/induct.ML
changeset 79827 e38f5f81592d
parent 78808 64973b03b778
child 80703 cc4ecaa8e96e