| Wed, 18 Aug 2010 11:55:27 +0200 |
haftmann |
added equality instantiation
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 15:32:06 +0200 |
haftmann |
dropped ancient infix mem; refined code generation operations in List.thy
|
file |
diff |
annotate
|
| Mon, 21 Jun 2010 09:06:14 +0200 |
haftmann |
extensionality rule fset_eqI
|
file |
diff |
annotate
|
| Mon, 24 May 2010 13:48:56 +0200 |
haftmann |
induction and case rules
|
file |
diff |
annotate
|
| Thu, 20 May 2010 18:00:48 +0200 |
haftmann |
proper code generator for complement
|
file |
diff |
annotate
|
| Thu, 20 May 2010 16:35:53 +0200 |
haftmann |
moved generic List operations to theory More_List
|
file |
diff |
annotate
|
| Wed, 19 May 2010 09:20:36 +0200 |
haftmann |
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
|
file |
diff |
annotate
|
| Thu, 22 Apr 2010 09:30:36 +0200 |
haftmann |
lemma dlist_ext
|
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, 11 Apr 2010 16:51:07 +0200 |
haftmann |
user interface for abstract datatypes is an attribute, not a command
|
file |
diff |
annotate
|
| Wed, 10 Mar 2010 15:29:22 +0100 |
haftmann |
avoid confusion
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 15:53:18 +0100 |
haftmann |
added Dlist
|
file |
diff |
annotate
|