src/HOL/Accessible_Part.thy
Wed, 11 Jul 2007 11:00:09 +0200 berghofe acc is now defined using inductive_set.
Wed, 07 Feb 2007 17:28:09 +0100 berghofe Adapted to new inductive definition package.
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Wed, 17 May 2006 01:23:40 +0200 wenzelm tuned source/document;
Fri, 05 May 2006 17:17:21 +0200 krauss First usable version of the new function definition package (HOL/function_packake/...).
less more (0) tip