| Mon, 11 Jul 2016 10:43:54 +0200 |
wenzelm |
more indentation for quasi_command keywords;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Thu, 03 Sep 2015 17:14:57 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 23:04:18 +0200 |
blanchet |
added flag to 'typedef' to allow concealed definitions
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 19:02:34 +0100 |
wenzelm |
declare minor keywords via theory header;
|
file |
diff |
annotate
|
| Tue, 08 Feb 2011 20:59:12 +0100 |
wenzelm |
discontinued obsolete alias HOL.thy for @{theory HOL} in ML;
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 16:44:24 +0200 |
haftmann |
dropped SML typedef_codegen: does not fit to code equations for record operations any longer
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 17:56:41 +0200 |
haftmann |
group record-related ML files
|
file |
diff |
annotate
|
| Tue, 20 Jul 2010 23:09:49 +0200 |
wenzelm |
discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| 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
|