| Thu, 05 Jul 2007 00:06:11 +0200 |
wenzelm |
added Tools/numeral.ML;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 18:00:57 +0200 |
chaieb |
Dependency on reflection_data.ML to build HOL-ex
|
file |
diff |
annotate
|
| Fri, 29 Jun 2007 18:21:25 +0200 |
paulson |
bug fixes to proof reconstruction
|
file |
diff |
annotate
|
| Tue, 26 Jun 2007 13:01:48 +0200 |
nipkow |
added NBE
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 12:16:27 +0200 |
krauss |
removed "sum_tools.ML" in favour of BalancedTree
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 20:48:48 +0200 |
wenzelm |
moved quantifier elimination tools to Tools/Qelim/;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 17:28:50 +0200 |
wenzelm |
renamed NatSimprocs.thy to Arith_Tools.thy;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 15:42:07 +0200 |
wenzelm |
replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 13:23:33 +0200 |
paulson |
integration of Metis prover
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 23:19:17 +0200 |
wenzelm |
added Tools/metis_tools.ML;
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 18:26:44 +0200 |
chaieb |
Added dependency on file Groebner_Basis.thy
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 11:05:59 +0200 |
chaieb |
Added new files for Presburger (cooper_data.ML, cooper.ML) and deleted old unused ones cooper_dec, cooper_proof, reflected_cooper etc..
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 21:24:35 +0200 |
urbanc |
take out Class.thy again, because it does not yet compile cleanly
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 16:12:08 +0200 |
chaieb |
New Reflected Presburger added to HOL/ex
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 22:46:55 +0200 |
wenzelm |
added ex/Groebner_Examples.thy;
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 20:46:25 +0200 |
chaieb |
Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 16:26:04 +0200 |
wenzelm |
Semiring normalization and Groebner Bases.
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 15:16:08 +0200 |
haftmann |
merged Code_Generator.thy into HOL.thy
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 09:56:19 +0200 |
urbanc |
included Class.thy in the compiling process for Nominal/Examples
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:41 +0200 |
wenzelm |
HOL-ex: tuned deps;
|
file |
diff |
annotate
|
| Fri, 01 Jun 2007 23:33:49 +0200 |
webertj |
tuned
|
file |
diff |
annotate
|
| Fri, 01 Jun 2007 23:21:40 +0200 |
webertj |
some tests for arith added
|
file |
diff |
annotate
|
| Fri, 01 Jun 2007 22:09:16 +0200 |
nipkow |
Moved list comprehension into List
|
file |
diff |
annotate
|
| Thu, 31 May 2007 20:55:31 +0200 |
wenzelm |
moved IsaPlanner from Provers to Tools;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:16:52 +0200 |
wenzelm |
moved Integ files to canonical place;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 13:18:52 +0200 |
wenzelm |
moved TFL files to canonical place;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 12:06:31 +0200 |
wenzelm |
moved Integ files to canonical place;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 10:17:23 +0200 |
urbanc |
included new example in the compiling process
|
file |
diff |
annotate
|
| Fri, 25 May 2007 18:08:34 +0200 |
nipkow |
Added List_Comprehension
|
file |
diff |
annotate
|
| Fri, 25 May 2007 05:18:56 +0200 |
urbanc |
took out Class.thy from the compiling process until memory problems are solved
|
file |
diff |
annotate
|