src/HOL/Tools/inductive_codegen.ML
changeset 19376 529b735edbf2
parent 19046 bc5c6c9b114e
child 19861 620d90091788
equal deleted inserted replaced
19375:8198a4ffff24 19376:529b735edbf2