Wed, 11 Jul 2007 11:16:34 +0200 |
berghofe |
Renamed inductive2 to inductive.
|
file |
diff |
annotate
|
Fri, 09 Mar 2007 08:45:58 +0100 |
haftmann |
resolved name clashes
|
file |
diff |
annotate
|
Mon, 11 Dec 2006 16:06:14 +0100 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
Fri, 05 May 2006 17:17:21 +0200 |
krauss |
First usable version of the new function definition package (HOL/function_packake/...).
|
file |
diff |
annotate
|
Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
Thu, 06 May 2004 20:43:30 +0200 |
schirmer |
tuned HOL/record package; enabled record_upd_simproc by default.
|
file |
diff |
annotate
|
Mon, 03 May 2004 23:22:17 +0200 |
schirmer |
reimplementation of HOL records; only one type is created for
|
file |
diff |
annotate
|
Wed, 14 May 2003 20:29:18 +0200 |
schirmer |
Adapted to changes in Map.thy
|
file |
diff |
annotate
|
Wed, 14 May 2003 10:22:09 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
Thu, 31 Oct 2002 18:27:10 +0100 |
schirmer |
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
|
file |
diff |
annotate
|
Thu, 26 Sep 2002 10:51:29 +0200 |
paulson |
Converted Fun to Isar style.
|
file |
diff |
annotate
|
Tue, 27 Aug 2002 11:03:05 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
Wed, 27 Feb 2002 08:52:09 +0100 |
schirmer |
Cleaning up the definition of static overriding.
|
file |
diff |
annotate
|
Mon, 25 Feb 2002 20:48:14 +0100 |
wenzelm |
clarified syntax of ``long'' statements: fixes/assumes/shows;
|
file |
diff |
annotate
|
Fri, 22 Feb 2002 11:26:44 +0100 |
schirmer |
Added check for field/method access to operational semantics and proved the acesses valid.
|
file |
diff |
annotate
|
Mon, 28 Jan 2002 23:35:20 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 28 Jan 2002 17:00:19 +0100 |
schirmer |
Isabelle/Bali sources;
|
file |
diff |
annotate
|