| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 15:32:24 +0200 |
haftmann |
tuned lemma formulations
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 17:21:48 +0100 |
hoelzl |
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 15:10:24 +0100 |
haftmann |
moved lemma map_of_zip_map to Map.thy
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 22:59:54 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Mon, 08 Jun 2009 08:38:50 +0200 |
haftmann |
using constant "chars"
|
file |
diff |
annotate
|
| Fri, 05 Jun 2009 13:35:11 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 18 May 2009 15:45:36 +0200 |
haftmann |
generalized lemma map_of_zip_map
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 08:14:24 +0100 |
haftmann |
Main is (Complex_Main) base entry point in library theories
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 08:23:11 +0100 |
haftmann |
stripped ID
|
file |
diff |
annotate
|
| Tue, 03 Feb 2009 21:26:21 +0100 |
haftmann |
handling type classes without parameters
|
file |
diff |
annotate
|
| Tue, 09 Dec 2008 12:53:25 -0800 |
huffman |
instantiation option :: (enum) enum
|
file |
diff |
annotate
|
| Fri, 24 Oct 2008 17:48:36 +0200 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 16:13:11 +0200 |
haftmann |
celver code lemma avoid type ambiguity problem with Haskell
|
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
|
| Fri, 23 May 2008 16:05:02 +0200 |
haftmann |
added code for quantifiers
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:59:27 +0200 |
berghofe |
Deleted instantiation "set :: (enum) enum"
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 08:33:16 +0200 |
haftmann |
constant HOL.eq now qualified
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:32 +0200 |
haftmann |
explicit class "eq" for operational equality
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 19:04:38 +0100 |
haftmann |
instance for functions, explicit characters
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 12:01:10 +0100 |
haftmann |
added theory Library/Enum.thy
|
file |
diff |
annotate
|