Wed, 18 Aug 2010 16:59:35 +0200 |
haftmann |
removed separate quickcheck_record module
|
file |
diff |
annotate
|
Tue, 17 Aug 2010 16:44:24 +0200 |
haftmann |
dropped SML typedef_codegen: does not fit to code equations for record operations any longer
|
file |
diff |
annotate
|
Tue, 17 Aug 2010 16:27:58 +0200 |
haftmann |
deleted typecopy package
|
file |
diff |
annotate
|
Thu, 12 Aug 2010 17:56:43 +0200 |
haftmann |
moved Record.thy from session Plain to Main; avoid variable name acc
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 12:05:48 +0200 |
blanchet |
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
|
file |
diff |
annotate
|
Tue, 03 Aug 2010 16:57:45 +0200 |
wenzelm |
renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
|
file |
diff |
annotate
|
Sun, 01 Aug 2010 10:15:44 +0200 |
bulwahn |
adding Code_Prolog theory to IsaMakefile and HOL-Library root file
|
file |
diff |
annotate
|
Thu, 29 Jul 2010 17:27:54 +0200 |
bulwahn |
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
|
file |
diff |
annotate
|
Wed, 28 Jul 2010 19:04:59 +0200 |
blanchet |
consequence of directory renaming
|
file |
diff |
annotate
|
Tue, 27 Jul 2010 17:56:01 +0200 |
blanchet |
rename "ATP_Manager" ML module to "Sledgehammer";
|
file |
diff |
annotate
|
Tue, 27 Jul 2010 17:43:11 +0200 |
blanchet |
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
|
file |
diff |
annotate
|
Mon, 26 Jul 2010 11:10:35 +0200 |
haftmann |
added Code_Natural.thy
|
file |
diff |
annotate
|
Wed, 21 Jul 2010 18:13:15 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
added new theories to IsaMakefile and ROOT.ML
|
file |
diff |
annotate
|
Wed, 21 Jul 2010 16:50:42 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
Mon, 19 Jul 2010 16:09:43 +0200 |
haftmann |
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
|
file |
diff |
annotate
|
Wed, 21 Jul 2010 15:44:36 +0200 |
wenzelm |
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
|
file |
diff |
annotate
|
Wed, 14 Jul 2010 14:16:12 +0200 |
haftmann |
load cache_io before code generator; moved adhoc-overloading to generic tools
|
file |
diff |
annotate
|
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
|
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
|
Wed, 24 Mar 2010 17:40:43 +0100 |
bulwahn |
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 |
boehmes |
more precise dependencies
|
file |
diff |
annotate
|
Wed, 24 Mar 2010 09:44:47 +0100 |
boehmes |
cache_io is now just a single ML file instead of a component
|
file |
diff |
annotate
|
Tue, 23 Mar 2010 19:35:03 +0100 |
wenzelm |
more accurate dependencies;
|
file |
diff |
annotate
|
Tue, 23 Mar 2010 16:17:41 +0100 |
hoelzl |
Generate image for HOL-Probability
|
file |
diff |
annotate
|
Mon, 22 Mar 2010 13:48:15 +0100 |
bulwahn |
merged
|
file |
diff |
annotate
|
Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
removed unused Predicate_Compile_Set
|
file |
diff |
annotate
|
Fri, 19 Mar 2010 15:07:44 +0100 |
blanchet |
move the Sledgehammer Isar commands together into one file;
|
file |
diff |
annotate
|
Fri, 19 Mar 2010 13:02:18 +0100 |
blanchet |
more Sledgehammer refactoring
|
file |
diff |
annotate
|
Tue, 16 Mar 2010 16:27:28 +0100 |
hoelzl |
Added product measure space
|
file |
diff |
annotate
|
Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
Wed, 17 Mar 2010 19:37:44 +0100 |
blanchet |
renamed "ATP_Linkup" theory to "Sledgehammer"
|
file |
diff |
annotate
|
Wed, 17 Mar 2010 18:16:31 +0100 |
blanchet |
move Sledgehammer files in a directory of their own
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 17:19:12 +0100 |
wenzelm |
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 |
haftmann |
merged
|
file |
diff |
annotate
|