| Wed, 12 May 2010 23:54:02 +0200 |
integrated SMT into the HOL image
|
file | diff | annotate |
| Wed, 12 May 2010 23:53:59 +0200 |
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 |
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 |
deleted SMT translation files (to be replaced by a simplified version)
|
file | diff | annotate |
| Wed, 12 May 2010 23:53:55 +0200 |
move the addition of extra facts into a separate module
|
file | diff | annotate |
| Tue, 11 May 2010 18:06:58 -0700 |
no more RealPow.thy (remaining lemmas moved to RealDef.thy)
|
file | diff | annotate |
| Tue, 11 May 2010 08:30:02 +0200 |
merged
|
file | diff | annotate |
| Mon, 10 May 2010 14:57:04 +0200 |
updated references to ML files
|
file | diff | annotate |
| Mon, 10 May 2010 13:58:18 +0200 |
less complex organization of cooper source code
|
file | diff | annotate |
| Mon, 10 May 2010 12:12:58 -0700 |
new construction of real numbers using Cauchy sequences
|
file | diff | annotate |
| Mon, 10 May 2010 11:30:05 -0700 |
put construction of reals using Dedekind cuts in HOL/ex
|
file | diff | annotate |
| Fri, 07 May 2010 16:12:26 +0200 |
renamed Normalizer to the more specific Semiring_Normalizer
|
file | diff | annotate |
| Fri, 07 May 2010 15:05:52 +0200 |
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 |
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
|
file | diff | annotate |
| Tue, 04 May 2010 18:19:24 +0200 |
Corrected imports; better approximation of dependencies.
|
file | diff | annotate |
| Tue, 04 May 2010 18:05:22 +0200 |
Add Convex to Library build
|
file | diff | annotate |
| Thu, 29 Apr 2010 11:42:34 -0700 |
merged
|
file | diff | annotate |
| Wed, 28 Apr 2010 16:11:07 -0700 |
move path-related stuff into new theory file
|
file | diff | annotate |
| Wed, 28 Apr 2010 15:07:03 -0700 |
add new Multivariate_Analysis files to IsaMakefile
|
file | diff | annotate |
| Thu, 29 Apr 2010 09:06:35 +0200 |
Tuning the quotient examples
|
file | diff | annotate |
| Mon, 26 Apr 2010 21:25:32 +0200 |
merge
|
file | diff | annotate |
| Fri, 23 Apr 2010 18:11:41 +0200 |
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 |
move the minimizer to the Sledgehammer directory
|
file | diff | annotate |
| Sat, 24 Apr 2010 13:31:52 -0700 |
document generation for Multivariate_Analysis
|
file | diff | annotate |
| Sat, 24 Apr 2010 11:11:09 -0700 |
move l2-norm stuff into separate theory file
|
file | diff | annotate |
| Fri, 23 Apr 2010 19:36:04 +0200 |
removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;
|
file | diff | annotate |
| Fri, 23 Apr 2010 10:00:53 +0200 |
Finite set theory
|
file | diff | annotate |
| Thu, 22 Apr 2010 22:01:06 +0200 |
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 |
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 |
removed rather toyish tree
|
file | diff | annotate |
| Thu, 08 Apr 2010 08:17:27 +0200 |
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
|
file | diff | annotate |
| Wed, 07 Apr 2010 17:24:44 +0200 |
Added Information theory and Example: dining cryptographers
|
file | diff | annotate |
| Thu, 01 Apr 2010 15:37:30 +0200 |
slightly more standard dependencies;
|
file | diff | annotate |
| Thu, 01 Apr 2010 10:27:06 +0200 |
merged
|
file | diff | annotate |
| Mon, 29 Mar 2010 15:50:18 +0200 |
get rid of Polyhash, since it's no longer used
|
file | diff | annotate |
| Mon, 29 Mar 2010 14:49:53 +0200 |
reintroduce efficient set structure to collect "no_atp" theorems
|
file | diff | annotate |
| Wed, 31 Mar 2010 16:44:41 +0200 |
putting compilation setup of predicate compiler in a separate file
|
file | diff | annotate |
| Mon, 29 Mar 2010 17:30:52 +0200 |
adding specialisation of predicates to the predicate compiler
|
file | diff | annotate |
| Thu, 25 Mar 2010 17:56:31 +0100 |
merged
|
file | diff | annotate |
| Wed, 24 Mar 2010 12:31:37 +0100 |
add new file "sledgehammer_util.ML" to setup
|
file | diff | annotate |
| Wed, 24 Mar 2010 22:30:33 +0100 |
more precise dependencies;
|
file | diff | annotate |
| Wed, 24 Mar 2010 17:41:25 +0100 |
merged
|
file | diff | annotate |
| Wed, 24 Mar 2010 17:40:44 +0100 |
removed predicate_compile_core.ML from HOL-ex session
|
file | diff | annotate |
| Wed, 24 Mar 2010 17:40:44 +0100 |
added predicate compiler quickcheck examples to new session Predicate_Compile_Examples
|
file | diff | annotate |
| Wed, 24 Mar 2010 17:40:43 +0100 |
moved further predicate compile files to HOL-Library
|
file | diff | annotate |
| Wed, 24 Mar 2010 17:40:43 +0100 |
moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
|
file | diff | annotate |
| Wed, 24 Mar 2010 12:30:21 +0100 |
more precise dependencies
|
file | diff | annotate |
| Wed, 24 Mar 2010 09:44:47 +0100 |
cache_io is now just a single ML file instead of a component
|
file | diff | annotate |
| Tue, 23 Mar 2010 19:35:03 +0100 |
more accurate dependencies;
|
file | diff | annotate |
| Tue, 23 Mar 2010 16:17:41 +0100 |
Generate image for HOL-Probability
|
file | diff | annotate |
| Mon, 22 Mar 2010 13:48:15 +0100 |
merged
|
file | diff | annotate |
| Mon, 22 Mar 2010 08:30:13 +0100 |
removed unused Predicate_Compile_Set
|
file | diff | annotate |
| Fri, 19 Mar 2010 15:07:44 +0100 |
move the Sledgehammer Isar commands together into one file;
|
file | diff | annotate |
| Fri, 19 Mar 2010 13:02:18 +0100 |
more Sledgehammer refactoring
|
file | diff | annotate |
| Tue, 16 Mar 2010 16:27:28 +0100 |
Added product measure space
|
file | diff | annotate |
| Thu, 18 Mar 2010 12:58:52 +0100 |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file | diff | annotate |
| Wed, 17 Mar 2010 19:37:44 +0100 |
renamed "ATP_Linkup" theory to "Sledgehammer"
|
file | diff | annotate |
| Wed, 17 Mar 2010 18:16:31 +0100 |
move Sledgehammer files in a directory of their own
|
file | diff | annotate |
| Sat, 13 Mar 2010 17:19:12 +0100 |
removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
|
file | diff | annotate |
| Thu, 11 Mar 2010 17:39:45 +0100 |
merged
|
file | diff | annotate |