| Mon, 26 Apr 2010 11:34:19 +0200 |
haftmann |
dropped group_simps, ring_simps, field_eq_simps
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 00:33:02 +0100 |
wenzelm |
cleanup type translations;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:15:27 +0100 |
wenzelm |
explicit @{type_syntax} markup;
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 14:00:43 +0100 |
haftmann |
combined former theories Divides and IntDiv to one theory Divides
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 00:36:12 +0200 |
wenzelm |
standardized basic operations on type option;
|
file |
diff |
annotate
|
| Sat, 09 May 2009 07:25:22 +0200 |
nipkow |
lemmas by Andreas Lochbihler
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 14:20:26 +0200 |
haftmann |
farewell to class recpower
|
file |
diff |
annotate
|
| Wed, 22 Apr 2009 19:09:21 +0200 |
haftmann |
power operation defined generic
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
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
|
| Fri, 13 Mar 2009 07:35:18 -0700 |
huffman |
fix typed print translation for CARD('a)
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 11:58:00 -0800 |
huffman |
class instances for num1
|
file |
diff |
annotate
|
| Thu, 19 Feb 2009 23:18:28 -0800 |
huffman |
cleaned up
|
file |
diff |
annotate
|
| Thu, 19 Feb 2009 17:13:35 -0800 |
huffman |
fix case_names
|
file |
diff |
annotate
|
| Thu, 19 Feb 2009 17:11:12 -0800 |
huffman |
nicer induction/cases rules for numeral types
|
file |
diff |
annotate
|
| Thu, 19 Feb 2009 16:51:46 -0800 |
huffman |
number_ring instances for numeral types
|
file |
diff |
annotate
|
| Mon, 26 Jan 2009 22:14:17 +0100 |
haftmann |
tuned header
|
file |
diff |
annotate
|
| Tue, 09 Dec 2008 15:31:38 -0800 |
huffman |
move lemmas from Numeral_Type.thy to other theories
|
file |
diff |
annotate
|
| Sun, 30 Nov 2008 18:10:00 +0100 |
huffman |
fix typed print translation for card UNIV
|
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, 02 Apr 2008 12:32:53 +0200 |
chaieb |
No longer imports InfiniteSet, ATP_Linkup is sufficient.
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 20:38:18 +0100 |
haftmann |
other UNIV lemmas
|
file |
diff |
annotate
|
| Fri, 23 Nov 2007 21:09:32 +0100 |
haftmann |
deleted card definition as code lemma; authentic syntax for card
|
file |
diff |
annotate
|
| Sat, 10 Nov 2007 18:36:06 +0100 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 16:08:00 +0200 |
wenzelm |
simplified type int (eliminated IntInf.int, integer);
|
file |
diff |
annotate
|
| Wed, 22 Aug 2007 20:59:19 +0200 |
huffman |
typed print translation for CARD('a);
|
file |
diff |
annotate
|
| Wed, 22 Aug 2007 18:53:54 +0200 |
huffman |
rename type pls to num0
|
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
|