| Mon, 23 Mar 2009 08:14:24 +0100 |
haftmann |
Main is (Complex_Main) base entry point in library theories
|
file |
diff |
annotate
|
| Sat, 14 Feb 2009 11:10:35 -0800 |
huffman |
add lemma surj_from_nat
|
file |
diff |
annotate
|
| Thu, 12 Feb 2009 11:04:22 -0800 |
huffman |
move countability proof from Rational to Countable; add instance rat :: countable
|
file |
diff |
annotate
|
| Tue, 03 Feb 2009 21:26:21 +0100 |
haftmann |
handling type classes without parameters
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 14:58:56 +0100 |
haftmann |
migrated class package to new locale implementation
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
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, 09 Apr 2008 05:31:04 +0200 |
huffman |
fix spelling
|
file |
diff |
annotate
|
| Tue, 08 Apr 2008 18:30:40 +0200 |
krauss |
Generic conversion and tactic "atomize_elim" to convert elimination rules
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 12:01:12 +0100 |
haftmann |
adjusted authorship
|
file |
diff |
annotate
|
| Mon, 10 Mar 2008 18:44:20 +0100 |
huffman |
instance fun :: (finite, countable) countable
|
file |
diff |
annotate
|
| Wed, 27 Feb 2008 21:41:07 +0100 |
haftmann |
added theory for countable types
|
file |
diff |
annotate
|