Tue, 11 May 2010 19:01:35 -0700 | huffman | include iszero_simps in semiring_norm just once (they are already included in rel_simps) | changeset | files |
Tue, 11 May 2010 19:00:32 -0700 | huffman | fix duplicate simp rule warning | changeset | files |
Tue, 11 May 2010 18:06:58 -0700 | huffman | no more RealPow.thy (remaining lemmas moved to RealDef.thy) | changeset | files |
Tue, 11 May 2010 17:20:11 -0700 | huffman | merged | changeset | files |
Tue, 11 May 2010 12:38:07 -0700 | huffman | simplify code for emptiness check | changeset | files |
Tue, 11 May 2010 12:05:19 -0700 | huffman | removed lemma real_sq_order; use power2_le_imp_le instead | changeset | files |
Tue, 11 May 2010 21:27:09 +0200 | haftmann | merged | changeset | files |
Tue, 11 May 2010 19:06:18 +0200 | haftmann | merged | changeset | files |