ProgTutorial/Package/Ind_Intro.thy
2012-04-30 Christian Urban removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
2011-11-07 Christian Urban tuned
less more (0) -2 tip