| Thu, 19 Sep 2019 17:24:08 +0100 |
paulson |
Tidying and one more theorem
|
file |
diff |
annotate
|
| Sat, 20 Apr 2019 18:02:22 +0000 |
haftmann |
follow convention of bold local syntax
|
file |
diff |
annotate
|
| Sat, 20 Apr 2019 18:02:22 +0000 |
haftmann |
more use of existing locales
|
file |
diff |
annotate
|
| Sat, 20 Apr 2019 18:02:21 +0000 |
haftmann |
avoid separate type class for mere definitional extension
|
file |
diff |
annotate
|
| Sat, 20 Apr 2019 18:02:20 +0000 |
haftmann |
tuned name
|
file |
diff |
annotate
|
| Sat, 01 Apr 2017 19:16:19 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 15:45:32 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 15:48:17 +0100 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
| Thu, 06 Aug 2015 14:29:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| 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
|