paulson [Wed, 02 Mar 2005 10:21:17 +0100] rev 15559
obscured the e-mail address lcp@cl
paulson [Wed, 02 Mar 2005 10:02:21 +0100] rev 15558
new lemmas int_diff_cases
huffman [Wed, 02 Mar 2005 00:56:41 +0100] rev 15557
eliminated deps for removed files
huffman [Wed, 02 Mar 2005 00:55:12 +0100] rev 15556
merged into Discrete.thy
huffman [Wed, 02 Mar 2005 00:54:06 +0100] rev 15555
converted to new-style theory
nipkow [Tue, 01 Mar 2005 18:48:52 +0100] rev 15554
integrated Jeremy's FiniteLib
kleing [Tue, 01 Mar 2005 05:44:13 +0100] rev 15553
spider dogding
obua [Mon, 28 Feb 2005 18:29:55 +0100] rev 15552
added setsum_diff1' which holds in more general cases than setsum_diff1
paulson [Mon, 28 Feb 2005 13:10:36 +0100] rev 15551
unfold theorems for trancl and rtrancl
dixon [Sun, 27 Feb 2005 00:00:40 +0100] rev 15550
lucas - added more comments and an extra type to clarify the code.
berghofe [Wed, 23 Feb 2005 15:19:00 +0100] rev 15549
Modified node_trans to avoid duplication of signature stamps
when undoing.
webertj [Wed, 23 Feb 2005 15:00:03 +0100] rev 15548
exception SAME removed
webertj [Wed, 23 Feb 2005 14:04:53 +0100] rev 15547
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
nipkow [Wed, 23 Feb 2005 10:23:22 +0100] rev 15546
suminf -> \<Sum>
dixon [Tue, 22 Feb 2005 18:42:22 +0100] rev 15545
Lucas - fixed bug in zero_var_indexes: it was ignoring vars in the flex-flex pairs. These are now taken into account.
paulson [Tue, 22 Feb 2005 13:05:47 +0100] rev 15544
removed redundant lemmas and simprules
nipkow [Tue, 22 Feb 2005 10:54:30 +0100] rev 15543
more setsum tuning
nipkow [Mon, 21 Feb 2005 19:23:46 +0100] rev 15542
more fine tuniung
nipkow [Mon, 21 Feb 2005 18:04:28 +0100] rev 15541
fixed proof
nipkow [Mon, 21 Feb 2005 15:57:45 +0100] rev 15540
removed superfluous setsum_constant
nipkow [Mon, 21 Feb 2005 15:04:10 +0100] rev 15539
comprehensive cleanup, replacing sumr by setsum
dixon [Sat, 19 Feb 2005 18:44:34 +0100] rev 15538
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
nipkow [Fri, 18 Feb 2005 15:20:27 +0100] rev 15537
continued eliminating sumr
nipkow [Fri, 18 Feb 2005 11:48:53 +0100] rev 15536
starting to get rid of sumr
nipkow [Fri, 18 Feb 2005 11:48:42 +0100] rev 15535
tuning
nipkow [Wed, 16 Feb 2005 19:00:49 +0100] rev 15534
*** empty log message ***
berghofe [Tue, 15 Feb 2005 16:56:15 +0100] rev 15533
refine now provides specific cases "goal1" ... "goaln" for addressing
subgoals of a proof state.
paulson [Mon, 14 Feb 2005 10:24:58 +0100] rev 15532
simplified a proof
skalberg [Sun, 13 Feb 2005 17:15:14 +0100] rev 15531
Deleted Library.option type.
berghofe [Fri, 11 Feb 2005 18:51:00 +0100] rev 15530
Fully qualified refl and trans to avoid confusion with theorems
in Lattice_Locales.partial_order.