| Wed, 28 Dec 2011 20:05:28 +0100 |
huffman |
restate some lemmas to respect int/bin distinction
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 19:15:28 +0100 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 18:50:35 +0100 |
huffman |
add lemma word_eq_iff
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 18:33:03 +0100 |
huffman |
restate lemma word_1_no in terms of Numeral1
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 12:52:23 +0100 |
huffman |
remove some duplicate lemmas
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 10:48:39 +0100 |
huffman |
simplify proof
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 10:30:43 +0100 |
huffman |
replace 'lemmas' with explicit 'lemma'
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 07:58:17 +0100 |
huffman |
add section headings
|
file |
diff |
annotate
|
| Tue, 27 Dec 2011 18:26:15 +0100 |
huffman |
remove duplicate lemma lists
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 20:03:13 +0100 |
wenzelm |
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
|
file |
diff |
annotate
|
| Tue, 27 Dec 2011 15:37:33 +0100 |
huffman |
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
|
file |
diff |
annotate
|
| Tue, 27 Dec 2011 13:16:22 +0100 |
huffman |
remove some uses of Int.succ and Int.pred
|
file |
diff |
annotate
|
| Tue, 27 Dec 2011 12:37:11 +0100 |
huffman |
remove redundant syntax declaration
|
file |
diff |
annotate
|
| Tue, 27 Dec 2011 11:38:55 +0100 |
huffman |
declare word_of_int_{0,1} [simp], for consistency with word_of_int_bin
|
file |
diff |
annotate
|
| Fri, 23 Dec 2011 16:37:27 +0100 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| Fri, 23 Dec 2011 15:55:23 +0100 |
huffman |
remove redundant lemma word_sub_def
|
file |
diff |
annotate
|
| Fri, 23 Dec 2011 11:50:12 +0100 |
huffman |
remove two conflicting simp rules for 'number_of (number_of _)' pattern
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 08:32:48 +0100 |
huffman |
replace 'lemmas' with 'lemma'
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 12:36:41 +0100 |
huffman |
towards removing BIT_simps from the simpset
|
file |
diff |
annotate
|
| Mon, 12 Dec 2011 08:19:37 +0100 |
huffman |
replace more uses of 'lemmas' with explicit 'lemma';
|
file |
diff |
annotate
|
| Sun, 11 Dec 2011 09:55:57 +0100 |
huffman |
replace many uses of 'lemmas' with 'lemma';
|
file |
diff |
annotate
|
| Sat, 10 Dec 2011 22:00:42 +0100 |
huffman |
prove class instances without extra lemmas
|
file |
diff |
annotate
|
| Sat, 10 Dec 2011 21:48:16 +0100 |
huffman |
finite class instance for word type; remove unused lemmas
|
file |
diff |
annotate
|
| Sat, 10 Dec 2011 21:07:59 +0100 |
huffman |
remove unused lemmas
|
file |
diff |
annotate
|
| Sat, 10 Dec 2011 16:24:22 +0100 |
huffman |
generalize some lemmas
|
file |
diff |
annotate
|
| Sat, 10 Dec 2011 08:29:19 +0100 |
huffman |
tidied Word.thy;
|
file |
diff |
annotate
|
| Fri, 09 Dec 2011 14:52:51 +0100 |
huffman |
remove redundant lemma word_diff_minus
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2011 22:59:39 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 20:59:30 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|