src/HOL/Tools/inductive_package.ML
changeset 23315 df3a7e9ebadb
parent 22997 d4f3b015b50b
child 23577 c5b93c69afd3
equal deleted inserted replaced
23314:6894137e854a 23315:df3a7e9ebadb