| Mon, 28 Jun 2010 15:32:06 +0200 |
haftmann |
dropped ancient infix mem; refined code generation operations in List.thy
|
file |
diff |
annotate
|
| Thu, 20 May 2010 16:40:29 +0200 |
haftmann |
renamed List_Set to the now more appropriate More_Set
|
file |
diff |
annotate
|
| Thu, 20 May 2010 16:35:54 +0200 |
haftmann |
added theory More_List
|
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
|
| Sun, 31 Jan 2010 19:07:03 +0100 |
haftmann |
adjusted to changes in List_Set.thy
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 14:54:13 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 14:54:01 +0100 |
haftmann |
merged Crude_Executable_Set into Executable_Set
|
file |
diff |
annotate
| base
|
| Mon, 26 Oct 2009 10:51:42 +0100 |
haftmann |
added SML_Quickcheck import
|
file |
diff |
annotate
|
| Tue, 06 Oct 2009 18:27:00 +0200 |
haftmann |
added Coset as constructor
|
file |
diff |
annotate
|
| Fri, 25 Sep 2009 09:50:31 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:32:53 +0200 |
haftmann |
explicitly hide empty, inter, union
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 11:34:21 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Sat, 19 Sep 2009 07:38:03 +0200 |
haftmann |
inter and union are mere abbreviations for inf and sup
|
file |
diff |
annotate
|
| Thu, 24 Sep 2009 18:29:29 +0200 |
haftmann |
subsumed by more general setup in List.thy
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 11:33:52 +0200 |
haftmann |
hide newly introduced constants
|
file |
diff |
annotate
|
| Fri, 18 Sep 2009 14:09:38 +0200 |
haftmann |
INTER and UNION are mere abbreviations for INFI and SUPR
|
file |
diff |
annotate
|
| Wed, 16 Sep 2009 13:43:05 +0200 |
haftmann |
Inter and Union are mere abbreviations for Inf and Sup
|
file |
diff |
annotate
|
| Wed, 22 Jul 2009 18:02:10 +0200 |
haftmann |
moved complete_lattice &c. into separate theory
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 12:18:56 +0200 |
haftmann |
Executable_Set is now a simple wrapper around Fset
|
file |
diff |
annotate
|
| 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
|