src/ZF/ind_syntax.ML
changeset 27760 3aa86edac080
parent 27261 5b3101338f42
child 28965 1de908189869