| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2012 17:18:55 +0200 |
wenzelm |
explicit is better than implicit;
|
file |
diff |
annotate
|
| Fri, 18 May 2012 15:08:08 +0200 |
kuncar |
don't generate code in Word because it breaks the current code setup
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 19:32:30 +0200 |
huffman |
add code lemmas for word operations
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 16:21:47 +1000 |
Thomas Sewell |
New tactic "word_bitwise" expands word equalities/inequalities into logic.
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 23:57:44 +0200 |
kuncar |
setup_lifting: no_code switch and supoport for quotient theorems
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 19:16:13 +0200 |
kuncar |
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 14:40:00 +0200 |
huffman |
remove now-unnecessary type annotations from lift_definition commands
|
file |
diff |
annotate
|
| Thu, 05 Apr 2012 16:25:59 +0200 |
huffman |
use standard quotient lemmas to generate transfer rules
|
file |
diff |
annotate
|
| Thu, 05 Apr 2012 14:14:16 +0200 |
huffman |
set up and use lift_definition for word operations
|
file |
diff |
annotate
|
| Thu, 05 Apr 2012 10:48:46 +0200 |
huffman |
configure transfer method for 'a word -> int
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 21:48:26 +0200 |
huffman |
mark some duplicate lemmas for deletion
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 15:51:53 +0100 |
huffman |
make more word theorems respect int/bin distinction
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 17:21:24 +0100 |
huffman |
remove ill-formed lemmas word_0_wi_Pls and word_m1_wi_Min
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 16:55:29 +0100 |
huffman |
avoid using Int.succ or Int.pred in proofs
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 13:50:37 +0100 |
huffman |
avoid using Int.Pls_def in proofs
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 13:37:23 +0100 |
huffman |
remove ill-formed lemmas word_pred_0_Min and word_m1_Min
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 13:33:03 +0100 |
huffman |
remove ill-formed lemma of_bl_no; adapt proofs
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 13:25:21 +0100 |
huffman |
adapt lemma mask_lem to respect int/bin distinction
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 16:09:16 +0100 |
huffman |
make more simp rules respect int/bin distinction
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 15:37:42 +0100 |
huffman |
make bool list functions respect int/bin distinction
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 13:16:18 +0100 |
huffman |
make uses of bin_sign respect int/bin distinction
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 12:45:00 +0100 |
huffman |
removed unnecessary lemma zero_bintrunc
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 12:24:34 +0100 |
huffman |
remove unnecessary lemmas
|
file |
diff |
annotate
|
| Wed, 08 Feb 2012 01:49:33 +0100 |
blanchet |
use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
|
file |
diff |
annotate
|
| Tue, 10 Jan 2012 15:43:16 +0100 |
huffman |
add simp rules for set_bit and msb applied to 0 and 1
|
file |
diff |
annotate
|
| Tue, 10 Jan 2012 14:48:42 +0100 |
huffman |
add simp rule test_bit_1
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 16:42:15 +0100 |
wenzelm |
recovered case syntax for of_int, also with source positions (appears to be unused nonetheless);
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 15:31:49 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Fri, 30 Dec 2011 16:08:35 +0100 |
huffman |
add simp rules for bitwise word operations with 1
|
file |
diff |
annotate
|
| Fri, 30 Dec 2011 11:11:57 +0100 |
huffman |
remove unnecessary intermediate lemmas
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 10:47:54 +0100 |
haftmann |
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 22:08:44 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 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
|