| Sun, 28 Jun 2009 11:02:27 +0200 |
haftmann |
Executable_Set now based on Code_Set
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 08:14:58 +0100 |
haftmann |
Main is (Complex_Main) base entry point in library theories
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 08:23:11 +0100 |
haftmann |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
file |
diff |
annotate
|
| Mon, 15 Dec 2008 10:16:38 +0100 |
nipkow |
flipped fold implementation
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 08:53:53 +0100 |
nipkow |
code for {x:A. P(x)} and for fold
|
file |
diff |
annotate
|
| Mon, 01 Dec 2008 14:56:08 +0100 |
haftmann |
added code equation for subset
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:33 +0200 |
haftmann |
only one theorem table for both code generators
|
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
|
| Wed, 07 May 2008 10:59:29 +0200 |
berghofe |
- Declared subset_eq as code lemma
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 22:34:26 +0100 |
wenzelm |
avoid rebinding of existing facts;
|
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:12 +0100 |
haftmann |
switched import from Main to List
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:14:20 +0200 |
haftmann |
overloaded definitions accompanied by explicit constants
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 21:47:39 +0200 |
haftmann |
uniform naming conventions for CG theories
|
file |
diff |
annotate
|