src/HOL/Tools/inductive_realizer.ML
changeset 60620 41e180848d02
parent 60362 befdc10ebb42
child 60752 b48830b670a1
equal deleted inserted replaced
60616:5a65c496d96f 60620:41e180848d02