src/HOL/Induct/Term.ML
changeset 9750 270cd9831e7b
parent 7847 5a3fa0c4b215
equal deleted inserted replaced
9749:36ddd544a18d 9750:270cd9831e7b