Fri, 30 Mar 2012 12:02:23 +0200 | huffman | restate various simp rules for word operations using pred_numeral | changeset | files |
Fri, 30 Mar 2012 11:52:26 +0200 | huffman | new lemmas for simplifying subtraction on nat numerals | changeset | files |
Fri, 30 Mar 2012 11:16:35 +0200 | huffman | removed redundant nat-specific copies of theorems | changeset | files |
Fri, 30 Mar 2012 10:41:27 +0200 | huffman | move more theorems from Nat_Numeral.thy to Num.thy | changeset | files |