ProgTutorial/Package/Ind_Extensions.thy
2009-10-13 Christian Urban tuned the ML-output mechanism; tuned slightly the text
less more (0) -1 tip