| Tue, 16 Sep 2008 16:13:09 +0200 |
haftmann |
a sophisticated char/nibble conversion combinator
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 09:21:27 +0200 |
haftmann |
explicit size of characters
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 20:38:17 +0200 |
haftmann |
distributed literal code generation out of central infrastructure
|
file |
diff |
annotate
|
| Mon, 01 Sep 2008 22:10:42 +0200 |
nipkow |
It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
|
file |
diff |
annotate
|
| Mon, 01 Sep 2008 19:16:40 +0200 |
nipkow |
cleaned up code generation for {.._} and {..<_}
|
file |
diff |
annotate
|
| Mon, 01 Sep 2008 10:18:37 +0200 |
haftmann |
restructured code generation of literals
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:09:20 +0200 |
haftmann |
restructured and split code serializer module
|
file |
diff |
annotate
|
| Fri, 01 Aug 2008 12:57:50 +0200 |
nipkow |
made setsum executable on int.
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 13:16:54 +0200 |
nipkow |
added removeAll
|
file |
diff |
annotate
|
| Sat, 28 Jun 2008 21:21:13 +0200 |
wenzelm |
@{lemma}: 'by' keyword;
|
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
|
| Fri, 23 May 2008 16:41:39 +0200 |
berghofe |
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
|
file |
diff |
annotate
|
| Mon, 12 May 2008 22:11:06 +0200 |
krauss |
Measure functions can now be declared via special rules, allowing for a
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:56:37 +0200 |
berghofe |
- Explicitely applied predicate1I in a few proofs, because it is no longer
|
file |
diff |
annotate
|
| Fri, 02 May 2008 18:01:02 +0200 |
nipkow |
Added documentation
|
file |
diff |
annotate
|
| Fri, 25 Apr 2008 16:28:06 +0200 |
krauss |
* New attribute "termination_simp": Simp rules for termination proofs
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 08:33:20 +0200 |
haftmann |
dropped some metis calls
|
file |
diff |
annotate
|
| 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
|