src/HOL/Tools/inductive_realizer.ML
changeset 42639 9d774c5d42a2
parent 42375 774df7c59508
child 43324 2b47822868e4
equal deleted inserted replaced
42638:a7a30721767a 42639:9d774c5d42a2