src/HOL/Bali/DefiniteAssignment.thy
Mon, 01 Aug 2011 12:08:53 +0200 nipkow infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
Fri, 18 Feb 2011 16:36:42 +0100 wenzelm modernized specifications;
Mon, 26 Jul 2010 17:41:26 +0200 wenzelm modernized/unified some specifications;
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Sat, 28 Jul 2007 20:40:22 +0200 wenzelm tuned ML/simproc declarations;
Wed, 11 Jul 2007 11:16:34 +0200 berghofe Renamed inductive2 to inductive.
Wed, 13 Jun 2007 00:01:41 +0200 wenzelm tuned proofs: avoid implicit prems;
Mon, 11 Dec 2006 16:06:14 +0100 berghofe Adapted to new inductive definition package.
Thu, 22 Dec 2005 00:28:41 +0100 wenzelm mutual induct with *.inducts;
Mon, 17 Oct 2005 23:10:13 +0200 wenzelm change_claset/simpset;
Thu, 22 Sep 2005 23:56:15 +0200 nipkow renamed rules to iprover
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Thu, 21 Apr 2005 22:02:06 +0200 wenzelm superceded by Pure.thy and CPure.thy;
Wed, 14 May 2003 20:29:18 +0200 schirmer Adapted to changes in Map.thy
Thu, 31 Oct 2002 18:27:10 +0100 schirmer "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
less more (0) tip