| Tue, 28 Jun 2005 15:27:45 +0200 |
paulson |
Constant "If" is now local
|
file |
diff |
annotate
|
| Mon, 16 May 2005 10:29:15 +0200 |
paulson |
Use of IntInf.int instead of int in most numeric simprocs; avoids
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 17:56:58 +0200 |
paulson |
fixed treatment of higher-order simprules
|
file |
diff |
annotate
|
| Mon, 07 Mar 2005 19:30:53 +0100 |
webertj |
refute_params: default value itself=1 added (for type classes)
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Fri, 10 Dec 2004 16:48:29 +0100 |
berghofe |
Moved code generator setup for product type to Product_Type.thy
|
file |
diff |
annotate
|
| Tue, 07 Dec 2004 16:16:10 +0100 |
paulson |
all theories must be related to Reconstruction
|
file |
diff |
annotate
|
| Fri, 20 Aug 2004 12:21:03 +0200 |
paulson |
proof reconstruction for external ATPs
|
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
|
| Mon, 19 Jul 2004 18:15:46 +0200 |
berghofe |
Moved code generator setup for lists to List.thy
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Wed, 26 May 2004 17:43:52 +0200 |
webertj |
new default parameters for refute
|
file |
diff |
annotate
|
| Fri, 26 Mar 2004 19:58:43 +0100 |
webertj |
satsolver=dpll
|
file |
diff |
annotate
|
| Wed, 10 Mar 2004 22:37:33 +0100 |
webertj |
changed default values for refute
|
file |
diff |
annotate
|
| Mon, 08 Mar 2004 11:12:06 +0100 |
paulson |
generic theorems about exponentials; general tidying up
|
file |
diff |
annotate
|
| Sat, 10 Jan 2004 13:35:10 +0100 |
webertj |
Adding 'refute' to HOL.
|
file |
diff |
annotate
|
| Mon, 22 Sep 2003 16:01:36 +0200 |
berghofe |
Improved efficiency of code generated for < predicate on natural numbers.
|
file |
diff |
annotate
|
| Fri, 11 Jul 2003 14:55:17 +0200 |
berghofe |
- Installed specific code generator for equality enforcing that
|
file |
diff |
annotate
|
| Tue, 27 May 2003 17:39:43 +0200 |
berghofe |
Added term_of function for product type.
|
file |
diff |
annotate
|
| Mon, 16 Dec 2002 13:43:11 +0100 |
berghofe |
Added mk_int and mk_list.
|
file |
diff |
annotate
|
| Sun, 21 Jul 2002 15:42:30 +0200 |
berghofe |
Added theory for setting up program extraction.
|
file |
diff |
annotate
|
| Tue, 16 Jul 2002 18:26:52 +0200 |
wenzelm |
moved stuff to List.thy;
|
file |
diff |
annotate
|
| Fri, 19 Apr 2002 14:51:33 +0200 |
berghofe |
code generator: wfrec combinator is now implemented by ML function wf_rec.
|
file |
diff |
annotate
|
| Thu, 20 Dec 2001 14:55:28 +0100 |
berghofe |
Declared characteristic equations for < on nat for code generation.
|
file |
diff |
annotate
|
| Mon, 10 Dec 2001 15:18:57 +0100 |
berghofe |
Tuned code generator setup.
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:35:11 +0100 |
wenzelm |
moved String into Main;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2001 16:28:26 +0200 |
berghofe |
Added code generator setup.
|
file |
diff |
annotate
|
| Wed, 08 Aug 2001 14:52:10 +0200 |
paulson |
Hilbert_Choice is needed only in Main itself
|
file |
diff |
annotate
|
| Fri, 24 Nov 2000 16:49:27 +0100 |
nipkow |
hide many names from Datatype_Universe.
|
file |
diff |
annotate
|