src/HOL/Bali/DefiniteAssignmentCorrect.thy
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Wed, 10 Feb 2010 00:50:36 +0100 wenzelm removed obsolete CVS Ids;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Mon, 21 Sep 2009 15:35:15 +0200 haftmann tuned proofs
Sat, 17 May 2008 21:46:24 +0200 wenzelm tuned proof;
Sun, 30 Sep 2007 21:55:15 +0200 wenzelm avoid internal names;
Sat, 28 Jul 2007 20:40:22 +0200 wenzelm tuned ML/simproc declarations;
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.
Mon, 11 Sep 2006 21:35:19 +0200 wenzelm induct method: renamed 'fixing' to 'arbitrary';
Wed, 02 Aug 2006 23:09:49 +0200 wenzelm tuned proofs;
Wed, 02 Aug 2006 22:27:08 +0200 wenzelm lemma da_good_approx: adapted induction (was exploting lifted obtain result);
Mon, 12 Jun 2006 20:58:25 +0200 wenzelm avoid accidental binding of ?Jmp;
Wed, 04 Jan 2006 19:22:53 +0100 nipkow Reversed Larry's option/iff change.
Thu, 22 Dec 2005 00:28:41 +0100 wenzelm mutual induct with *.inducts;
Wed, 21 Dec 2005 12:02:57 +0100 paulson removed or modified some instances of [iff]
Fri, 25 Nov 2005 18:58:35 +0100 wenzelm removed obsolete dummy paragraphs;
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, 19 Feb 2004 15:57:34 +0100 ballarin Efficient, graph-based reasoner for linear and partial orders.
Wed, 14 May 2003 20:29:18 +0200 schirmer Adapted to changes in Map.thy
Sat, 08 Feb 2003 14:46:22 +0100 nipkow adjusted dom rules
Fri, 01 Nov 2002 13:16:28 +0100 schirmer Inserted some extra paragraphs in large proofs to make tex run...
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