| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 15:15:32 +0100 |
haftmann |
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
|
file |
diff |
annotate
|
| Sun, 24 Aug 2008 14:42:24 +0200 |
haftmann |
default replaces arbitrary
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 23:50:33 +0100 |
wenzelm |
modernized primrec;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 18:30:11 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 16:05:42 +0200 |
nipkow |
rules -> iprover
|
file |
diff |
annotate
|
| Fri, 08 Jul 2005 11:38:53 +0200 |
nipkow |
proof needed updating because of arith
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Mon, 21 Oct 2002 17:23:23 +0200 |
berghofe |
Eta contraction is now switched off when printing extracted program.
|
file |
diff |
annotate
|
| Wed, 07 Aug 2002 16:50:08 +0200 |
berghofe |
Removed (now unneeded) declaration of realizer for induction on datatype b.
|
file |
diff |
annotate
|
| Sun, 21 Jul 2002 15:44:42 +0200 |
berghofe |
Examples for program extraction in HOL.
|
file |
diff |
annotate
|