src/HOL/Tools/inductive_codegen.ML
changeset 27723 ce8f79b91ed1
parent 27398 768da1da59d6
child 27809 a1e409db516b
equal deleted inserted replaced
27722:d657036e26c5 27723:ce8f79b91ed1