Wed, 09 Apr 2008 05:30:14 +0200 |
huffman |
move lemmas from Word/BinBoolList.thy to List.thy
|
file |
diff |
annotate
|
Sat, 29 Mar 2008 19:14:00 +0100 |
wenzelm |
replaced 'ML_setup' by 'ML';
|
file |
diff |
annotate
|
Thu, 27 Mar 2008 19:04:36 +0100 |
haftmann |
restructuring; explicit case names for rule list_induct2
|
file |
diff |
annotate
|
Mon, 17 Mar 2008 18:37:00 +0100 |
wenzelm |
removed duplicate lemmas;
|
file |
diff |
annotate
|
Tue, 26 Feb 2008 20:38:13 +0100 |
haftmann |
char and nibble are finite
|
file |
diff |
annotate
|
Tue, 26 Feb 2008 11:18:43 +0100 |
bulwahn |
Added useful general lemmas from the work with the HeapMonad
|
file |
diff |
annotate
|
Fri, 15 Feb 2008 17:36:21 +0100 |
nipkow |
more lemmas
|
file |
diff |
annotate
|
Fri, 25 Jan 2008 14:54:44 +0100 |
haftmann |
dropped superfluous code theorems
|
file |
diff |
annotate
|
Thu, 10 Jan 2008 19:09:21 +0100 |
berghofe |
New interface for test data generators.
|
file |
diff |
annotate
|
Mon, 10 Dec 2007 11:24:03 +0100 |
haftmann |
swtiched ATP_Linkup and PreList in theory hierarchy
|
file |
diff |
annotate
|
Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
Thu, 06 Dec 2007 17:05:44 +0100 |
haftmann |
temporary code generator work arounds
|
file |
diff |
annotate
|
Thu, 06 Dec 2007 16:36:19 +0100 |
haftmann |
authentic primrec
|
file |
diff |
annotate
|
Thu, 29 Nov 2007 17:08:26 +0100 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
Mon, 05 Nov 2007 22:49:28 +0100 |
kleing |
rev_nth
|
file |
diff |
annotate
|
Mon, 05 Nov 2007 18:18:39 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
Mon, 05 Nov 2007 08:31:12 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
Sun, 28 Oct 2007 13:18:00 +0100 |
wenzelm |
append/member: more light-weight way to declare authentic syntax;
|
file |
diff |
annotate
|
Sat, 27 Oct 2007 15:53:23 +0200 |
krauss |
use "fun" for definition of "member" -> authentic syntax
|
file |
diff |
annotate
|
Tue, 23 Oct 2007 23:27:23 +0200 |
nipkow |
went back to >0
|
file |
diff |
annotate
|
Tue, 23 Oct 2007 13:10:19 +0200 |
paulson |
random tidying of proofs
|
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
|
Sun, 21 Oct 2007 14:21:45 +0200 |
wenzelm |
avoid very slow metis invocation;
|
file |
diff |
annotate
|
Sat, 20 Oct 2007 12:09:33 +0200 |
chaieb |
fixed proofs
|
file |
diff |
annotate
|
Thu, 18 Oct 2007 16:09:36 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Wed, 17 Oct 2007 18:09:38 +0200 |
nipkow |
added sorted_list_of_set
|
file |
diff |
annotate
|
Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|
Mon, 08 Oct 2007 16:28:29 +0200 |
berghofe |
list_codegen and char_codegen now call invoke_tycodegen to ensure
|
file |
diff |
annotate
|
Mon, 01 Oct 2007 19:21:32 +0200 |
haftmann |
added some lemmas
|
file |
diff |
annotate
|
Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|