new
deleting after discussion on isabelle-usr
improved documentation
new inference rule trivial_cases