| Tue, 14 Jul 2009 16:27:32 +0200 |
haftmann |
prefer code_inline over code_unfold; use code_unfold_post where appropriate
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Thu, 14 May 2009 15:09:47 +0200 |
haftmann |
preprocessing must consider eq
|
file |
diff |
annotate
|
| Sat, 09 May 2009 07:25:22 +0200 |
nipkow |
lemmas by Andreas Lochbihler
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 20:30:17 +0100 |
haftmann |
moved instance option :: finite to Option.thy
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:48:52 +0100 |
nipkow |
Option.thy
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 10:03:25 +0200 |
haftmann |
split off Option theory
|
file |
diff |
annotate
|
| Tue, 30 May 2000 18:02:49 +0200 |
berghofe |
the is now defined using primrec, avoiding explicit use of arbitrary.
|
file |
diff |
annotate
|
| Wed, 09 Sep 1998 17:23:42 +0200 |
oheimb |
AddIffs[not_None_eq];
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:03:20 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| Tue, 24 Mar 1998 15:51:37 +0100 |
oheimb |
added o2s
|
file |
diff |
annotate
|
| Mon, 10 Nov 1997 14:57:31 +0100 |
oheimb |
replaced 8bit characters
|
file |
diff |
annotate
|
| Tue, 04 Nov 1997 20:48:38 +0100 |
oheimb |
added the, option_map, and case analysis theorems
|
file |
diff |
annotate
|
| Tue, 24 Sep 1996 09:02:34 +0200 |
nipkow |
Moved Option out of IOA into core HOL
|
file |
diff |
annotate
|