src/HOL/IMP/Abs_Int3.thy
Mon, 11 Mar 2013 12:27:31 +0100 nipkow more factorisation of Step & Co
Sun, 10 Mar 2013 10:10:01 +0100 nipkow termination proof for narrowing: fewer assumptions
Fri, 08 Mar 2013 11:28:04 +0100 nipkow simplified basic termination proof
Wed, 06 Mar 2013 16:10:56 +0100 nipkow major redesign: order instead of preorder, new definition of intervals as quotients
Fri, 22 Feb 2013 20:12:53 +0100 nipkow more abstract intervals
Tue, 12 Feb 2013 11:54:29 +0100 nipkow tuned top
Fri, 25 Jan 2013 16:45:09 +0100 nipkow tuned
Sat, 19 Jan 2013 21:05:05 +0100 nipkow simplified proofs
Wed, 17 Oct 2012 14:58:04 +0200 wenzelm proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;
Wed, 26 Sep 2012 03:16:40 +0200 nipkow tuned
Wed, 26 Sep 2012 03:03:11 +0200 nipkow added counterexamples
Tue, 25 Sep 2012 07:37:42 +0200 nipkow tuned
Mon, 24 Sep 2012 14:22:07 +0200 nipkow generalized types
Mon, 24 Sep 2012 06:58:09 +0200 nipkow tuned termination proof
Fri, 21 Sep 2012 13:39:30 +0200 nipkow more termination proofs
Mon, 17 Sep 2012 02:25:38 +0200 nipkow tuned
Sun, 16 Sep 2012 11:50:03 +0200 nipkow converted wt into a set, tuned names
Fri, 07 Sep 2012 07:20:55 +0200 nipkow adjusted examples
Mon, 03 Sep 2012 15:41:06 +0200 nipkow added annotations after condition in if and while
Fri, 10 Aug 2012 17:17:05 +0200 nipkow Improved complete lattice formalisation - no more index set.
Thu, 19 Apr 2012 20:19:13 +0200 nipkow added revised version of Abs_Int
less more (0) tip