src/ZF/ind_syntax.ML
changeset 12551 f44734e5e746
parent 12243 a2c0aaf94460
child 13150 0c50d13d449a
equal deleted inserted replaced
12550:32843ad8160a 12551:f44734e5e746