| Wed, 22 Feb 2012 17:34:31 +0100 |
huffman |
tuned whitespace
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Sun, 27 Nov 2011 23:10:19 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 17:22:49 -0700 |
huffman |
avoid warnings
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 17:23:15 +0200 |
wenzelm |
misc tuning -- eliminated old-fashioned rep_thm;
|
file |
diff |
annotate
|
| Fri, 07 May 2010 15:36:03 +0200 |
krauss |
spelling
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 10:29:48 +0200 |
haftmann |
Table.map replaces Table.map'
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 15:46:08 +0200 |
wenzelm |
disposed some old debugging tools;
|
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, 19 Aug 2010 16:08:59 +0200 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 15:32:17 +0200 |
haftmann |
explicit is better than implicit
|
file |
diff |
annotate
|
| Tue, 25 May 2010 20:28:16 +0200 |
wenzelm |
eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
|
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 16:32:20 +0200 |
haftmann |
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 17:58:58 +0100 |
wenzelm |
tuned header;
|
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
|
| Mon, 19 Oct 2009 21:54:57 +0200 |
wenzelm |
uniform use of Integer.add/mult/sum/prod;
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 23:27:05 +0200 |
wenzelm |
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
|
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
|
| Wed, 26 Aug 2009 11:40:28 +0200 |
boehmes |
added further conversions and conversionals
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:01:41 +0200 |
wenzelm |
renamed functor TableFun to Table, and GraphFun to Graph;
|
file |
diff |
annotate
|
| Tue, 12 May 2009 17:32:50 +0100 |
chaieb |
A generic arithmetic prover based on Positivstellensatz certificates --- also implements Fourrier-Motzkin elimination as a special case Fourrier-Motzkin elimination
|
file |
diff |
annotate
|