| Wed, 30 Jun 2010 16:28:13 +0200 |
haftmann |
use existing bit type from theory Bit
|
file |
diff |
annotate
|
| Thu, 24 Jun 2010 21:04:35 +0200 |
haftmann |
more direct definition simplifies proofs
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:30 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 22 Sep 2009 15:36:55 +0200 |
haftmann |
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 19:43:19 +0200 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 24 Apr 2009 17:45:15 +0200 |
haftmann |
funpow and relpow with shared "^^" syntax
|
file |
diff |
annotate
|
| Mon, 20 Apr 2009 09:32:07 +0200 |
haftmann |
power operation on functions with syntax o^; power operation on relations with syntax ^^
|
file |
diff |
annotate
|
| Fri, 17 Apr 2009 08:34:52 +0200 |
haftmann |
zmod_zmult_zmult1 now subsumed by mod_mult_mult1
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 09:58:26 +0100 |
nipkow |
removed redundant thms
|
file |
diff |
annotate
|
| Mon, 26 Jan 2009 22:14:18 +0100 |
haftmann |
stripped Id
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:00:50 -0800 |
huffman |
fixed proofs due to changes in Int.thy
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:59:42 +0200 |
berghofe |
Deleted subset_antisym in a few proofs, because it is
|
file |
diff |
annotate
|
| Fri, 04 Apr 2008 13:40:24 +0200 |
haftmann |
more new primrec
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:36 +0200 |
haftmann |
tuned towards code generation
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 07:15:40 +0100 |
kleing |
fixed broken bintrunc lemma
|
file |
diff |
annotate
|
| Sun, 17 Feb 2008 06:49:53 +0100 |
huffman |
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
| Thu, 08 Nov 2007 20:08:00 +0100 |
wenzelm |
eliminated illegal schematic variables in where/of;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:53:44 +0200 |
nipkow |
Eliminated most of the neq0_conv occurrences. As a result, many
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 20:13:47 +0200 |
huffman |
revert to Word library version from 2007/08/20
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 00:37:12 +0200 |
huffman |
remove unused lemmas
|
file |
diff |
annotate
|
| Thu, 23 Aug 2007 23:37:51 +0200 |
huffman |
remove lemma bin_rec_PM
|
file |
diff |
annotate
|
| Thu, 23 Aug 2007 18:52:44 +0200 |
huffman |
import BinInduct;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2007 15:47:42 +0200 |
huffman |
move bin_nth stuff to its own subsection
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 17:24:57 +0200 |
huffman |
move BIT datatype stuff from Num_Lemmas to BinGeneral
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 17:20:41 +0200 |
huffman |
simplify termination proof
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 22:48:24 +0200 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 21:31:10 +0200 |
huffman |
reorganize into subsections
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:11:09 +0200 |
huffman |
headers for document generation
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 04:34:31 +0200 |
kleing |
* HOL-Word:
|
file |
diff |
annotate
|