src/ZF/ind_syntax.ML
changeset 33008 b0ff69f0a248
parent 32960 69916a850301
child 33317 b4534348b8fd