src/HOL/Tools/inductive_codegen.ML
changeset 27793 29ad1d91a5a3
parent 27398 768da1da59d6
child 27809 a1e409db516b
equal deleted inserted replaced
27792:e4a4d057749d 27793:29ad1d91a5a3