| Tue, 03 Feb 2009 21:26:21 +0100 |
haftmann |
handling type classes without parameters
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
no base sort in class import
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 00:42:52 +0100 |
wenzelm |
misc tuning and modernisation;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 10:58:01 +0200 |
wenzelm |
LocalTheory.exit_global;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 19:57:45 +0200 |
huffman |
add lemma Abs_image
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:56:50 +0200 |
berghofe |
Deleted instantiation "set :: (type) itself".
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 20:38:16 +0100 |
haftmann |
class itself works around a problem with class interpretation in class finite
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:15:48 +0100 |
haftmann |
interpretation of typedefs
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 23:05:55 +0200 |
huffman |
remove redundant assumption from Rep_range lemma
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 17:30:51 +0200 |
haftmann |
removed proof dependency on transitivity theorems
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 14:38:24 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 15:16:08 +0200 |
haftmann |
merged Code_Generator.thy into HOL.thy
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2006 14:31:13 +0200 |
haftmann |
added typecopy_package
|
file |
diff |
annotate
|
| Mon, 24 Apr 2006 16:37:52 +0200 |
haftmann |
seperated typedef codegen from main code
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Tue, 26 Oct 2004 16:31:09 +0200 |
berghofe |
Added setup for code generator.
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Wed, 24 Jul 2002 22:15:55 +0200 |
wenzelm |
simplified locale predicates;
|
file |
diff |
annotate
|
| Wed, 24 Jul 2002 00:10:52 +0200 |
wenzelm |
predicate defs via locales;
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:33:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 30 Oct 2001 13:43:26 +0100 |
wenzelm |
lemma Least_mono moved from Typedef.thy to Set.thy;
|
file |
diff |
annotate
|
| Sun, 28 Oct 2001 22:59:12 +0100 |
wenzelm |
converted theory "Set";
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:08:29 +0200 |
wenzelm |
moved rulify to ObjectLogic;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2001 21:43:00 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 03 Oct 2001 21:03:05 +0200 |
wenzelm |
Tools/induct_attrib.ML now part of Pure;
|
file |
diff |
annotate
|
| Wed, 03 Oct 2001 20:54:05 +0200 |
wenzelm |
moved linorder_cases to theory Ord;
|
file |
diff |
annotate
|
| Thu, 27 Sep 2001 22:26:00 +0200 |
wenzelm |
renamed theory "subset" to "Typedef";
|
file |
diff |
annotate
|