src/HOL/Tools/inductive_codegen.ML
changeset 40607 30d512bf47a7
parent 40132 7ee65dbffa31
child 40911 7febf76e0a69
equal deleted inserted replaced
40606:af1a0b0c6202 40607:30d512bf47a7