| 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
|
| Wed, 28 Apr 2010 15:07:03 -0700 |
huffman |
add new Multivariate_Analysis files to IsaMakefile
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 09:06:35 +0200 |
Cezary Kaliszyk |
Tuning the quotient examples
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 21:25:32 +0200 |
blanchet |
merge
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 18:11:41 +0200 |
blanchet |
now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 17:38:25 +0200 |
blanchet |
move the minimizer to the Sledgehammer directory
|
file |
diff |
annotate
|
| Sat, 24 Apr 2010 13:31:52 -0700 |
huffman |
document generation for Multivariate_Analysis
|
file |
diff |
annotate
|
| Sat, 24 Apr 2010 11:11:09 -0700 |
huffman |
move l2-norm stuff into separate theory file
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 19:36:04 +0200 |
wenzelm |
removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 10:00:53 +0200 |
Cezary Kaliszyk |
Finite set theory
|
file |
diff |
annotate
|
| Thu, 22 Apr 2010 22:01:06 +0200 |
wenzelm |
split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 12:27:14 +0200 |
haftmann |
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 17:46:42 +0200 |
haftmann |
removed rather toyish tree
|
file |
diff |
annotate
|
| Thu, 08 Apr 2010 08:17:27 +0200 |
bulwahn |
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 17:24:44 +0200 |
hoelzl |
Added Information theory and Example: dining cryptographers
|
file |
diff |
annotate
|
| Thu, 01 Apr 2010 15:37:30 +0200 |
wenzelm |
slightly more standard dependencies;
|
file |
diff |
annotate
|
| Thu, 01 Apr 2010 10:27:06 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 15:50:18 +0200 |
blanchet |
get rid of Polyhash, since it's no longer used
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 14:49:53 +0200 |
blanchet |
reintroduce efficient set structure to collect "no_atp" theorems
|
file |
diff |
annotate
|
| Wed, 31 Mar 2010 16:44:41 +0200 |
bulwahn |
putting compilation setup of predicate compiler in a separate file
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 17:30:52 +0200 |
bulwahn |
adding specialisation of predicates to the predicate compiler
|
file |
diff |
annotate
|
| Thu, 25 Mar 2010 17:56:31 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 12:31:37 +0100 |
blanchet |
add new file "sledgehammer_util.ML" to setup
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 22:30:33 +0100 |
wenzelm |
more precise dependencies;
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 17:41:25 +0100 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 17:40:44 +0100 |
bulwahn |
removed predicate_compile_core.ML from HOL-ex session
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 17:40:44 +0100 |
bulwahn |
added predicate compiler quickcheck examples to new session Predicate_Compile_Examples
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 17:40:43 +0100 |
bulwahn |
moved further predicate compile files to HOL-Library
|
file |
diff |
annotate
|