src/HOL/Tools/inductive_realizer.ML
changeset 61448 25e40e78f6d4
parent 60826 695cf1fab6cc
child 62922 96691631c1eb
equal deleted inserted replaced
61447:7cf8b604280f 61448:25e40e78f6d4