src/HOL/Tools/inductive_codegen.ML
changeset 33726 0878aecbf119
parent 33522 737589bb9bb8
child 33771 17926df64f0f
equal deleted inserted replaced
33725:a8481da77270 33726:0878aecbf119