src/HOL/Tools/inductive_codegen.ML
changeset 39388 fdbb2c55ffc2
parent 39253 0c47d615a69b
child 40132 7ee65dbffa31
equal deleted inserted replaced
39387:6608c4838ff9 39388:fdbb2c55ffc2