doc-src/TutorialI/Inductive/Star.thy
Thu, 19 Jul 2007 15:35:00 +0200 berghofe Refer to major premise of induction rule via "thm_style prem1".
less more (0) -10 -1 tip