src/HOL/Tools/inductive_codegen.ML
changeset 37087 dd47971b9875
parent 36960 01594f816e3a
child 37198 3af985b10550
equal deleted inserted replaced
37086:3a7c2c949320 37087:dd47971b9875