src/HOL/Tools/inductive_codegen.ML
changeset 41477 be6d903e5943
parent 41448 72ba43b47c7f
child 41472 f6ab14e61604