src/HOL/Tools/inductive.ML
changeset 62128 3201ddb00097
parent 62093 bd73a2279fcd
child 62969 9f394a16c557
equal deleted inserted replaced
62127:d8e7738bd2e9 62128:3201ddb00097