src/HOL/Tools/inductive_package.ML
changeset 14472 cba7c0a3ffb3
parent 14235 281295a1bbaa
child 14643 130076a81b84
equal deleted inserted replaced
14471:5688b05b2575 14472:cba7c0a3ffb3