src/HOL/Tools/inductive_realizer.ML
changeset 14135 f8a25218b423
parent 13928 d572aeea3ff3
child 14888 99ac3eb0f84e
equal deleted inserted replaced
14134:0fdf5708c7a8 14135:f8a25218b423