| Tue, 13 Jul 2010 00:15:37 +0200 |
krauss |
uniform do notation for monads
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 00:15:37 +0200 |
krauss |
generic ad-hoc overloading via check/uncheck
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 21:38:37 +0200 |
wenzelm |
moved misc legacy stuff from OldGoals to Misc_Legacy;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 20:35:10 +0200 |
wenzelm |
removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 16:40:48 +0200 |
haftmann |
dropped empty theory
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 16:19:15 +0200 |
haftmann |
split off mrec into separate theory
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:27 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:12 +0200 |
haftmann |
more regular session structure
|
file |
diff |
annotate
|
| Sat, 10 Jul 2010 22:39:16 +0200 |
wenzelm |
regular image setup for HOL-Library (cf. 4915de09b4d3 and ccae4ecd67f4) -- note that document preparation requires a separate session directory, and library.ML is a bit too generic as a file in the default load path;
|
file |
diff |
annotate
|
| Fri, 09 Jul 2010 17:15:03 +0200 |
krauss |
moved example to its own file in HOL/ex
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:28:18 +0200 |
haftmann |
more accurate dependencies
|
file |
diff |
annotate
|
| 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
|
| Wed, 12 May 2010 23:54:04 +0200 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:02 +0200 |
boehmes |
integrated SMT into the HOL image
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:53:59 +0200 |
boehmes |
split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:53:57 +0200 |
boehmes |
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:53:56 +0200 |
boehmes |
deleted SMT translation files (to be replaced by a simplified version)
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:53:55 +0200 |
boehmes |
move the addition of extra facts into a separate module
|
file |
diff |
annotate
|
| Tue, 11 May 2010 18:06:58 -0700 |
huffman |
no more RealPow.thy (remaining lemmas moved to RealDef.thy)
|
file |
diff |
annotate
|
| Tue, 11 May 2010 08:30:02 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 10 May 2010 14:57:04 +0200 |
haftmann |
updated references to ML files
|
file |
diff |
annotate
|
| Mon, 10 May 2010 13:58:18 +0200 |
haftmann |
less complex organization of cooper source code
|
file |
diff |
annotate
|
| Mon, 10 May 2010 12:12:58 -0700 |
huffman |
new construction of real numbers using Cauchy sequences
|
file |
diff |
annotate
|
| Mon, 10 May 2010 11:30:05 -0700 |
huffman |
put construction of reals using Dedekind cuts in HOL/ex
|
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 16:32:20 +0200 |
haftmann |
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
|
file |
diff |
annotate
|
| Tue, 04 May 2010 18:19:24 +0200 |
hoelzl |
Corrected imports; better approximation of dependencies.
|
file |
diff |
annotate
|
| Tue, 04 May 2010 18:05:22 +0200 |
hoelzl |
Add Convex to Library build
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 11:42:34 -0700 |
huffman |
merged
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 16:11:07 -0700 |
huffman |
move path-related stuff into new theory file
|
file |
diff |
annotate
|