Wed, 02 Mar 2005 10:33:10 +0100 lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
dixon [Wed, 02 Mar 2005 10:33:10 +0100] rev 15560
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
Wed, 02 Mar 2005 10:21:17 +0100 obscured the e-mail address lcp@cl
paulson [Wed, 02 Mar 2005 10:21:17 +0100] rev 15559
obscured the e-mail address lcp@cl
Wed, 02 Mar 2005 10:02:21 +0100 new lemmas int_diff_cases
paulson [Wed, 02 Mar 2005 10:02:21 +0100] rev 15558
new lemmas int_diff_cases
Wed, 02 Mar 2005 00:56:41 +0100 eliminated deps for removed files
huffman [Wed, 02 Mar 2005 00:56:41 +0100] rev 15557
eliminated deps for removed files
Wed, 02 Mar 2005 00:55:12 +0100 merged into Discrete.thy
huffman [Wed, 02 Mar 2005 00:55:12 +0100] rev 15556
merged into Discrete.thy
Wed, 02 Mar 2005 00:54:06 +0100 converted to new-style theory
huffman [Wed, 02 Mar 2005 00:54:06 +0100] rev 15555
converted to new-style theory
Tue, 01 Mar 2005 18:48:52 +0100 integrated Jeremy's FiniteLib
nipkow [Tue, 01 Mar 2005 18:48:52 +0100] rev 15554
integrated Jeremy's FiniteLib
Tue, 01 Mar 2005 05:44:13 +0100 spider dogding
kleing [Tue, 01 Mar 2005 05:44:13 +0100] rev 15553
spider dogding
Mon, 28 Feb 2005 18:29:55 +0100 added setsum_diff1' which holds in more general cases than setsum_diff1
obua [Mon, 28 Feb 2005 18:29:55 +0100] rev 15552
added setsum_diff1' which holds in more general cases than setsum_diff1
Mon, 28 Feb 2005 13:10:36 +0100 unfold theorems for trancl and rtrancl
paulson [Mon, 28 Feb 2005 13:10:36 +0100] rev 15551
unfold theorems for trancl and rtrancl
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip