| Sat, 19 Nov 2016 19:43:09 +0100 |
wenzelm |
avoid import of Complex_Main into Word library (amending 34b7e2da95f6), e.g. to avoid intrusion of const "ii" into theories without complex numbers;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 09:33:54 +0200 |
nipkow |
"split add" -> "split"
|
file |
diff |
annotate
|
| Fri, 15 Jul 2016 12:23:51 +0200 |
eberlm |
Tuned Bool_List_Representation
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 13:49:37 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 23 Mar 2016 09:37:38 +1100 |
kleing |
HOL-Word: add stronger bl_to_bin_lt2p_drop
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 16:54:06 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 14:24:23 +1000 |
Thomas Sewell |
Hypsubst preserves equality hypotheses
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 07:07:07 +0100 |
nipkow |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
|
file |
diff |
annotate
|
| Sat, 28 Dec 2013 21:06:26 +0100 |
haftmann |
move instantiation here from AFP/Native_Word
|
file |
diff |
annotate
|
| Sat, 28 Dec 2013 21:06:22 +0100 |
haftmann |
cleanup
|
file |
diff |
annotate
|
| Fri, 27 Dec 2013 20:35:32 +0100 |
haftmann |
tuned proofs and declarations
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Mon, 23 Dec 2013 18:37:51 +0100 |
haftmann |
prefer "Bits" as theory name for abstract bit operations, similar to "Orderings", "Lattices", "Groups" etc.
|
file |
diff |
annotate
|
| Mon, 23 Dec 2013 14:24:21 +0100 |
haftmann |
syntactically tuned
|
file |
diff |
annotate
|
| Mon, 23 Dec 2013 14:24:20 +0100 |
haftmann |
prefer plain bool over dedicated type for binary digits
|
file |
diff |
annotate
|
| Fri, 06 Sep 2013 20:59:36 +0200 |
haftmann |
slight cleanup of lemma locations; tuned proof
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 15:29:50 +0200 |
haftmann |
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 12:02:23 +0200 |
huffman |
restate various simp rules for word operations using pred_numeral
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 16:59:20 +0100 |
huffman |
avoid using Int.succ_def in proofs
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 16:53:59 +0100 |
huffman |
avoid using BIT_simps in proofs;
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 16:46:43 +0100 |
huffman |
avoid using BIT_simps in 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 15:37:42 +0100 |
huffman |
make bool list functions respect int/bin distinction
|
file |
diff |
annotate
|
| Tue, 17 Jan 2012 16:30:54 +0100 |
huffman |
factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
|
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 12:27:06 +0100 |
huffman |
use 'induct arbitrary' instead of 'rule_format' attribute
|
file |
diff |
annotate
|
| Tue, 27 Dec 2011 12:05:03 +0100 |
huffman |
declare simp rules immediately, instead of using 'declare' commands
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 14:39:14 +0100 |
huffman |
replace many uses of 'lemmas' with explicit 'lemma'
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 12:36:41 +0100 |
huffman |
towards removing BIT_simps from the simpset
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 12:05:47 +0100 |
huffman |
remove some unwanted numeral-representation-specific simp rules
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 20:59:30 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Thu, 17 Nov 2011 12:29:48 +0100 |
huffman |
HOL-Word: add simp rules for bin_rest, bin_last; shorten several proofs
|
file |
diff |
annotate
|
| Sat, 12 Nov 2011 13:01:56 +0100 |
huffman |
removed some old-style semicolons
|
file |
diff |
annotate
|
| Fri, 16 Sep 2011 12:10:43 +1000 |
kleing |
removed unused legacy lemma names, some comment cleanup.
|
file |
diff |
annotate
|
| Fri, 25 Feb 2011 14:25:41 +0100 |
nipkow |
added simp lemma nth_Cons_pos to List
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 13:32:14 +0200 |
haftmann |
avoid bitstrings in generated code
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 16:45:47 +0200 |
haftmann |
more speaking names
|
file |
diff |
annotate
| base
|