Sat, 19 Dec 2020 17:49:14 +0000 |
haftmann |
more precise simpset for method unat_arith
|
file |
diff |
annotate
|
Sat, 05 Dec 2020 19:24:36 +0000 |
haftmann |
moved some lemmas from AFP to distribution
|
file |
diff |
annotate
|
Thu, 26 Nov 2020 18:09:02 +0000 |
paulson |
Stepan Holub's stronger version of comm_append_are_replicate, and a de-applied Word.thy
|
file |
diff |
annotate
|
Sun, 15 Nov 2020 10:13:03 +0000 |
haftmann |
official collection for bit projection simplifications
|
file |
diff |
annotate
|
Thu, 29 Oct 2020 10:03:03 +0000 |
haftmann |
moved most material from session HOL-Word to Word_Lib in the AFP
|
file |
diff |
annotate
| base
|
Tue, 02 Mar 2010 12:26:50 +0100 |
krauss |
killed more recdefs
|
file |
diff |
annotate
|
Wed, 17 Feb 2010 10:30:36 -0800 |
huffman |
fix more looping simp rules
|
file |
diff |
annotate
|
Thu, 21 Jan 2010 09:27:57 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
Sat, 16 Jan 2010 17:15:28 +0100 |
haftmann |
dropped some old primrecs and some constdefs
|
file |
diff |
annotate
|
Sun, 10 Jan 2010 18:43:45 +0100 |
berghofe |
Adapted to changes in induct method.
|
file |
diff |
annotate
|
Fri, 30 Oct 2009 13:59:50 +0100 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
Mon, 31 Aug 2009 14:09:42 +0200 |
nipkow |
tuned the simp rules for Int involving insert and intervals.
|
file |
diff |
annotate
|
Fri, 28 Aug 2009 19:35:49 +0200 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|
Wed, 22 Apr 2009 19:09:21 +0200 |
haftmann |
power operation defined generic
|
file |
diff |
annotate
|
Tue, 03 Mar 2009 17:05:18 +0100 |
nipkow |
removed and renamed redundant lemmas
|
file |
diff |
annotate
|
Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
Tue, 16 Sep 2008 09:21:26 +0200 |
haftmann |
dropped superfluous code lemmas
|
file |
diff |
annotate
|
Mon, 07 Jul 2008 08:47:17 +0200 |
haftmann |
absolute imports of HOL/*.thy theories
|
file |
diff |
annotate
|
Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
Tue, 10 Jun 2008 15:30:56 +0200 |
haftmann |
removed some dubious code lemmas
|
file |
diff |
annotate
|
Sat, 29 Mar 2008 22:55:49 +0100 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
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
|
Fri, 25 Jan 2008 14:53:52 +0100 |
haftmann |
moved definition of power on ints to theory Int
|
file |
diff |
annotate
|
Tue, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
Mon, 10 Dec 2007 11:24:12 +0100 |
haftmann |
switched import from Main to List
|
file |
diff |
annotate
|
Tue, 23 Oct 2007 23:27:23 +0200 |
nipkow |
went back to >0
|
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
|
Sat, 20 Oct 2007 12:09:33 +0200 |
chaieb |
fixed proofs
|
file |
diff |
annotate
|
Tue, 17 Jul 2007 14:38:00 +0200 |
krauss |
reverted fun->recdef, since there are problems with induction rule
|
file |
diff |
annotate
|