src/HOL/Tools/inductive_realizer.ML
changeset 33061 e3e61133e0fc
parent 33040 cffdb7b28498
child 33171 292970b42770