| Mon, 25 Oct 2010 21:17:16 +0200 |
bulwahn |
adding new predicate compiler files to the IsaMakefile
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 13:36:20 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 13:34:57 +0200 |
haftmann |
moved sledgehammer to Plain; tuned dependencies
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 11:42:05 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 10:30:46 +0200 |
blanchet |
introduced manual version of "Auto Solve" as "solve_direct"
|
file |
diff |
annotate
|
| Sat, 23 Oct 2010 23:42:04 +0200 |
krauss |
integrated partial_function into HOL-Plain
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 18:38:59 +0200 |
bulwahn |
splitting Hotel Key card example into specification and the two tests for counter example generation
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 13:54:51 +0200 |
blanchet |
renamed files
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 11:10:37 +0200 |
blanchet |
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 10:28:11 +0200 |
blanchet |
factor out "Meson_Tactic" from "Meson_Clausify"
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 22:45:09 +0200 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 22:01:34 +0200 |
blanchet |
added "Meson" theory to Makefile
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 21:37:42 +0200 |
blanchet |
move MESON files together
|
file |
diff |
annotate
|
| Wed, 29 Sep 2010 23:26:39 +0200 |
blanchet |
rename file
|
file |
diff |
annotate
|
| Wed, 29 Sep 2010 09:07:58 +0200 |
haftmann |
moved old_primrec source to nominal package, where it is still used
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 15:39:59 +0200 |
haftmann |
dropped old primrec package
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 12:47:55 +0200 |
haftmann |
modernized session
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 10:44:08 +0200 |
blanchet |
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 14:50:18 +0200 |
bulwahn |
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 15:10:21 +0200 |
haftmann |
Factored out ML into separate file
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 16:38:11 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 16:24:23 +0200 |
blanchet |
added new "Metis_Reconstruct" module, temporarily empty
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 16:12:02 +0200 |
blanchet |
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 10:52:35 +0200 |
boehmes |
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 11:12:08 +0200 |
blanchet |
factored out TSTP/SPASS/Vampire proof parsing;
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 20:47:14 +0200 |
wenzelm |
dropped obsolete src/Tools/random_word.ML -- superseded by src/Tools/Metis/src/Random.sml stemming from the Metis distribution;
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 15:35:01 +0200 |
haftmann |
more accurate dependencies
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 13:44:10 +0200 |
haftmann |
more accurate dependencies
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 21:24:10 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Sat, 11 Sep 2010 10:28:44 +0200 |
blanchet |
start renaming "Auto_Counterexample" to "Auto_Tools";
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 14:54:02 +0200 |
haftmann |
print mode for Imperative HOL overview; tuned and more accurate dependencies
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 09:56:28 +0200 |
haftmann |
more correct dependencies
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 16:01:06 +0200 |
blanchet |
merge
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 17:51:26 +0200 |
blanchet |
remove "minipick" (the toy version of Nitpick) and some tests;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 11:52:43 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 11:51:53 +0200 |
bulwahn |
adding the Reg_Exp example
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 11:51:53 +0200 |
bulwahn |
adding IMP quickcheck examples
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 11:51:53 +0200 |
bulwahn |
adding the CFG example to the build process
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 11:51:53 +0200 |
bulwahn |
adding a List example (challenge from Tobias) for counterexample search
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 11:51:53 +0200 |
bulwahn |
adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 14:18:16 +0200 |
wenzelm |
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 13:22:11 +0200 |
wenzelm |
modernized session ROOT setup;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 17:12:16 +0200 |
wenzelm |
just one refute.ML;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 08:29:30 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 23:52:59 +0200 |
blanchet |
move file
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 23:46:23 +0200 |
blanchet |
shorten a few file names
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 12:01:19 +0200 |
haftmann |
factored out generic part of Scala serializer into code_namespace.ML
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 07:53:31 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 08:00:51 +0200 |
bulwahn |
adding Lambda example theory; tuned
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 20:24:28 +0200 |
blanchet |
"try" -- a new diagnosis tool that tries to apply several methods in parallel
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 16:59:49 +0200 |
bulwahn |
adding hotel keycard example for prolog generation
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 19:35:57 +0200 |
hoelzl |
Rewrite the Probability theory.
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 17:48:30 +0200 |
haftmann |
split and enriched theory SetsAndFunctions
|
file |
diff |
annotate
|
| 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
|