| Sat, 15 May 2010 17:59:06 +0200 |
wenzelm |
incorporated further conversions and conversionals, after some minor tuning;
|
file |
diff |
annotate
|
| Fri, 07 May 2010 16:12:26 +0200 |
haftmann |
renamed Normalizer to the more specific Semiring_Normalizer
|
file |
diff |
annotate
|
| Fri, 07 May 2010 15:05:52 +0200 |
haftmann |
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
|
file |
diff |
annotate
|
| Thu, 06 May 2010 23:11:57 +0200 |
haftmann |
former free-floating field_comp_conv now in structure Normalizer
|
file |
diff |
annotate
|
| Thu, 06 May 2010 19:27:51 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 06 May 2010 16:32:20 +0200 |
haftmann |
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 22:20:59 -0700 |
huffman |
remove redundant lemma vector_dist_norm
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:08:52 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:02:56 +0200 |
haftmann |
curried union as canonical list operation
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 10:15:31 +0200 |
haftmann |
removed old-style \ and \\ infixes
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:16:25 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 00:36:12 +0200 |
wenzelm |
standardized basic operations on type option;
|
file |
diff |
annotate
|
| Wed, 14 Oct 2009 22:57:44 +0200 |
wenzelm |
eliminated obsolete C/flip combinator;
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 13:32:03 +0200 |
Philipp Meyer |
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
|
file |
diff |
annotate
|
| Mon, 21 Sep 2009 15:05:26 +0200 |
Philipp Meyer |
sos method generates and uses proof certificates
|
file |
diff |
annotate
|
| Wed, 26 Aug 2009 11:40:28 +0200 |
boehmes |
added further conversions and conversionals
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 16:11:36 -0700 |
huffman |
add extra type constraints for dist, norm
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 14:32:00 -0700 |
huffman |
generalize norm method to work over class real_normed_vector
|
file |
diff |
annotate
|
| Fri, 29 May 2009 15:32:33 -0700 |
huffman |
instance ^ :: (metric_space, finite) metric_space
|
file |
diff |
annotate
|
| Thu, 28 May 2009 22:54:57 -0700 |
huffman |
fix reference to dist_def
|
file |
diff |
annotate
|
| Tue, 12 May 2009 17:32:49 +0100 |
chaieb |
Isolated decision procedure for noms and the general arithmetic solver
|
file |
diff |
annotate
|
| Sun, 05 Apr 2009 19:21:51 +0100 |
chaieb |
fixed usage of rational constants
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 10:01:58 +0100 |
haftmann |
attempt to bypass spurious infix syntax problem on polyml/sun
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 16:57:10 +0000 |
chaieb |
Fixed theorem reference
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 16:43:52 +0000 |
chaieb |
A generic decision procedure for linear rea arithmetic and normed vector spaces
|
file |
diff |
annotate
|