src/HOL/Bali/DefiniteAssignment.thy
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