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".
Wed, 11 Jul 2007 10:53:39 +0200 berghofe Adapted to new inductive definition package.
Wed, 19 Oct 2005 21:52:07 +0200 wenzelm fix headers;
less more (0) -10 -3 tip