src/HOL/Tools/inductive_realizer.ML
changeset 68423 c1db7503dbaa
parent 67316 adaf279ce67b
child 69593 3dda49e08b9d
equal deleted inserted replaced
68421:e082a36dc35d 68423:c1db7503dbaa