src/Tools/induct.ML
changeset 79720 deb3056ed823
parent 78808 64973b03b778
child 80703 cc4ecaa8e96e