src/HOL/Tools/inductive_codegen.ML
changeset 14182 5f49f00fe084
parent 14163 5ffa75ce4919
child 14195 e7c9206dd2ef
equal deleted inserted replaced
14181:942db403d4bb 14182:5f49f00fe084