src/HOL/Tools/inductive_codegen.ML
changeset 43445 270bbbcda059
parent 43324 2b47822868e4
child 43619 3803869014aa
equal deleted inserted replaced
43444:f744902b4681 43445:270bbbcda059