| Fri, 27 Dec 2013 14:35:14 +0100 |
haftmann |
prefer target-style syntaxx for sublocale
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:43 +0100 |
haftmann |
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
|
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
|
| Thu, 19 Feb 2009 12:37:03 -0800 |
huffman |
declare xor_compl_{left,right} [simp]
|
file |
diff |
annotate
|
| Mon, 26 Jan 2009 22:14:17 +0100 |
haftmann |
tuned header
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Tue, 18 Dec 2007 14:37:00 +0100 |
haftmann |
switched from PreList to ATP_Linkup
|
file |
diff |
annotate
|
| Mon, 10 Dec 2007 11:24:09 +0100 |
haftmann |
switched import from Main to PreList
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 17:48:04 +0100 |
ballarin |
Type instance of thm mk_left_commute in locales.
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 20:53:37 +0200 |
huffman |
declare conj_absorb [simp]
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 20:38:32 +0200 |
huffman |
cleaned up; declared more simp rules
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 00:22:18 +0200 |
kleing |
boolean algebras as locales and numbers as types by Brian Huffman
|
file |
diff |
annotate
|