Nominal/Ex/Height.thy
2011-01-19 Christian Urban defined height as a function that returns an integer
2010-12-31 Christian Urban added proper case names for all induct and exhaust theorems
2010-12-31 Christian Urban added small example for strong inductions; functions still need a sorry
less more (0) tip