src/HOL/Tools/inductive_realizer.ML
changeset 33235 cbe96b3cb3d0
parent 33171 292970b42770
child 33244 db230399f890
equal deleted inserted replaced
33234:a5eba0447559 33235:cbe96b3cb3d0