| Fri, 26 Nov 2010 22:04:33 +0100 |
wenzelm |
just one version of fold_rev2;
|
file |
diff |
annotate
|
| Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 10:29:48 +0200 |
haftmann |
Table.map replaces Table.map'
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 17:09:18 +0200 |
wenzelm |
Sum_Of_Squares: proper configuration options;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
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
|
| Mon, 26 Apr 2010 11:34:19 +0200 |
haftmann |
dropped group_simps, ring_simps, field_eq_simps
|
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
|
| Thu, 26 Nov 2009 20:07:02 +0100 |
Philipp Meyer |
fixed csdp output parser
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 15:20:54 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 21:15:33 +0200 |
wenzelm |
use plain Scan.repeat (NB: Scan.bulk is for cascading sources -- mostly interna use);
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 13:48:06 +0200 |
haftmann |
map_range (and map_index) combinator
|
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 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
|
| Tue, 20 Oct 2009 20:54:31 +0200 |
wenzelm |
uniform use of Integer.min/max;
|
file |
diff |
annotate
|
| Mon, 19 Oct 2009 21:54:57 +0200 |
wenzelm |
uniform use of Integer.add/mult/sum/prod;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 21:08:03 +0200 |
wenzelm |
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 20:47:26 +0200 |
wenzelm |
tuned header;
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 20:33:45 +0200 |
wenzelm |
core_sos_tac: SUBPROOF body operates on subgoal 1;
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 11:54:01 +0200 |
Philipp Meyer |
changed core_sos_tac to use SUBPROOF
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 14:10:36 +0200 |
Philipp Meyer |
replaced and tuned uses of foldr1
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 13:48:00 +0200 |
Philipp Meyer |
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
|
file |
diff |
annotate
|
| Tue, 22 Sep 2009 14:17:54 +0200 |
Philipp Meyer |
removed opening of structures
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2009 11:26:46 +0200 |
Philipp Meyer |
used standard fold function and type aliases
|
file |
diff |
annotate
|
| Mon, 21 Sep 2009 15:05:26 +0200 |
Philipp Meyer |
sos method generates and uses proof certificates
|
file |
diff |
annotate
|
| Thu, 06 Aug 2009 19:51:59 +0200 |
wenzelm |
misc changes to SOS by Philipp Meyer:
|
file |
diff |
annotate
| base
|