src/HOL/Induct/Exp.ML
changeset 5760 7e2cf2820684
parent 5223 4cb05273f764
child 6141 a6922171b396