src/HOL/Tools/inductive_realizer.ML
changeset 60149 9b0825a00b1a
parent 59582 0fbed69ff081
child 60362 befdc10ebb42
equal deleted inserted replaced
60148:f0fc2378a479 60149:9b0825a00b1a