| Thu, 08 Jul 2010 16:17:44 +0200 |
haftmann |
tuned tabs
|
file |
diff |
annotate
|
| Fri, 02 Jul 2010 14:23:16 +0200 |
haftmann |
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 19:14:54 +0200 |
wenzelm |
avoid Old_Number_Theory;
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 11:48:42 +0200 |
hoelzl |
Add theory for indicator function.
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 08:12:55 +0200 |
haftmann |
repaired line ending
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 17:12:38 +0200 |
haftmann |
one unified Word theory
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 16:46:44 +0200 |
haftmann |
more speaking names
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 16:28:14 +0200 |
haftmann |
more speaking theory names
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 18:05:36 +0200 |
blanchet |
factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 17:08:39 +0200 |
blanchet |
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 16:42:06 +0200 |
blanchet |
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 16:15:03 +0200 |
blanchet |
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
|
file |
diff |
annotate
|
| Thu, 24 Jun 2010 11:08:21 +0200 |
wenzelm |
more accurate dependencies;
|
file |
diff |
annotate
|
| Tue, 22 Jun 2010 23:54:02 +0200 |
blanchet |
factor out TPTP format output into file of its own, to facilitate further changes
|
file |
diff |
annotate
|
| Mon, 21 Jun 2010 19:33:51 +0200 |
hoelzl |
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
|
file |
diff |
annotate
|
| Tue, 15 Jun 2010 14:28:22 +0200 |
haftmann |
added code_simp infrastructure
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 21:12:28 +0200 |
wenzelm |
replaced ML pokes by explicit usedir -p;
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 16:24:14 +0200 |
haftmann |
HOL-Proofs is based in Main.thy
|
file |
diff |
annotate
|
| Tue, 25 May 2010 22:21:31 +0200 |
wenzelm |
moved ML files where they are actually used;
|
file |
diff |
annotate
|
| Tue, 25 May 2010 21:49:44 +0200 |
wenzelm |
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
|
file |
diff |
annotate
|
| Thu, 20 May 2010 16:40:29 +0200 |
haftmann |
renamed List_Set to the now more appropriate More_Set
|
file |
diff |
annotate
|
| Thu, 20 May 2010 16:35:53 +0200 |
haftmann |
adjusted
|
file |
diff |
annotate
|
| Mon, 17 May 2010 10:58:31 +0200 |
haftmann |
dropped old Library/Word.thy and toy example ex/Adder.thy
|
file |
diff |
annotate
|
| Sat, 15 May 2010 18:11:00 +0200 |
wenzelm |
moved normarith.ML where it is actually used;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 17:59:06 +0200 |
wenzelm |
incorporated further conversions and conversionals, after some minor tuning;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 15:07:39 +0200 |
wenzelm |
more precise dependencies for HOL-Word-SMT_Examples;
|
file |
diff |
annotate
|
| Fri, 14 May 2010 15:09:37 +0200 |
blanchet |
move Refute dependency from Plain to Main
|
file |
diff |
annotate
|
| Fri, 14 May 2010 15:07:53 +0200 |
blanchet |
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
|
file |
diff |
annotate
|
| Thu, 13 May 2010 00:44:48 +0200 |
boehmes |
more precise dependencies
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:06 +0200 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|