| Tue, 07 Sep 2010 11:51:53 +0200 |
adding the CFG example to the build process
|
file | diff | annotate |
| Tue, 07 Sep 2010 11:51:53 +0200 |
adding a List example (challenge from Tobias) for counterexample search
|
file | diff | annotate |
| Tue, 07 Sep 2010 11:51:53 +0200 |
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 |
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 |
modernized session ROOT setup;
|
file | diff | annotate |
| Thu, 02 Sep 2010 17:12:16 +0200 |
just one refute.ML;
|
file | diff | annotate |
| Thu, 02 Sep 2010 08:29:30 +0200 |
merged
|
file | diff | annotate |
| Tue, 31 Aug 2010 23:52:59 +0200 |
move file
|
file | diff | annotate |
| Tue, 31 Aug 2010 23:46:23 +0200 |
shorten a few file names
|
file | diff | annotate |
| Wed, 01 Sep 2010 12:01:19 +0200 |
factored out generic part of Scala serializer into code_namespace.ML
|
file | diff | annotate |
| Wed, 01 Sep 2010 07:53:31 +0200 |
merged
|
file | diff | annotate |
| Tue, 31 Aug 2010 08:00:51 +0200 |
adding Lambda example theory; tuned
|
file | diff | annotate |
| Tue, 31 Aug 2010 20:24:28 +0200 |
"try" -- a new diagnosis tool that tries to apply several methods in parallel
|
file | diff | annotate |
| Wed, 25 Aug 2010 16:59:49 +0200 |
adding hotel keycard example for prolog generation
|
file | diff | annotate |
| Mon, 23 Aug 2010 19:35:57 +0200 |
Rewrite the Probability theory.
|
file | diff | annotate |
| Fri, 20 Aug 2010 17:48:30 +0200 |
split and enriched theory SetsAndFunctions
|
file | diff | annotate |
| Wed, 18 Aug 2010 16:59:35 +0200 |
removed separate quickcheck_record module
|
file | diff | annotate |
| Tue, 17 Aug 2010 16:44:24 +0200 |
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 |
deleted typecopy package
|
file | diff | annotate |
| Thu, 12 Aug 2010 17:56:43 +0200 |
moved Record.thy from session Plain to Main; avoid variable name acc
|
file | diff | annotate |
| Mon, 09 Aug 2010 12:05:48 +0200 |
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
|
file | diff | annotate |
| Tue, 03 Aug 2010 16:57:45 +0200 |
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 |
adding Code_Prolog theory to IsaMakefile and HOL-Library root file
|
file | diff | annotate |
| Thu, 29 Jul 2010 17:27:54 +0200 |
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 |
consequence of directory renaming
|
file | diff | annotate |
| Tue, 27 Jul 2010 17:56:01 +0200 |
rename "ATP_Manager" ML module to "Sledgehammer";
|
file | diff | annotate |
| Tue, 27 Jul 2010 17:43:11 +0200 |
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
|
file | diff | annotate |
| Mon, 26 Jul 2010 11:10:35 +0200 |
added Code_Natural.thy
|
file | diff | annotate |
| Wed, 21 Jul 2010 18:13:15 +0200 |
merged
|
file | diff | annotate |
| Wed, 21 Jul 2010 18:11:51 +0200 |
added new theories to IsaMakefile and ROOT.ML
|
file | diff | annotate |
| Wed, 21 Jul 2010 16:50:42 +0200 |
merged
|
file | diff | annotate |
| Wed, 21 Jul 2010 15:44:36 +0200 |
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
|
file | diff | annotate |
| Mon, 19 Jul 2010 16:09:43 +0200 |
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
|
file | diff | annotate |
| Wed, 14 Jul 2010 14:16:12 +0200 |
load cache_io before code generator; moved adhoc-overloading to generic tools
|
file | diff | annotate |
| Tue, 13 Jul 2010 00:15:37 +0200 |
uniform do notation for monads
|
file | diff | annotate |
| Tue, 13 Jul 2010 00:15:37 +0200 |
generic ad-hoc overloading via check/uncheck
|
file | diff | annotate |
| Mon, 12 Jul 2010 21:38:37 +0200 |
moved misc legacy stuff from OldGoals to Misc_Legacy;
|
file | diff | annotate |
| Mon, 12 Jul 2010 20:35:10 +0200 |
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 |
dropped empty theory
|
file | diff | annotate |
| Mon, 12 Jul 2010 16:19:15 +0200 |
split off mrec into separate theory
|
file | diff | annotate |
| Mon, 12 Jul 2010 08:58:27 +0200 |
merged
|
file | diff | annotate |
| Mon, 12 Jul 2010 08:58:12 +0200 |
more regular session structure
|
file | diff | annotate |
| Sat, 10 Jul 2010 22:39:16 +0200 |
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 |
moved example to its own file in HOL/ex
|
file | diff | annotate |
| Thu, 08 Jul 2010 16:28:18 +0200 |
more accurate dependencies
|
file | diff | annotate |
| Thu, 08 Jul 2010 16:17:44 +0200 |
tuned tabs
|
file | diff | annotate |
| Fri, 02 Jul 2010 14:23:16 +0200 |
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
|
file | diff | annotate |
| Thu, 01 Jul 2010 19:14:54 +0200 |
avoid Old_Number_Theory;
|
file | diff | annotate |
| Thu, 01 Jul 2010 11:48:42 +0200 |
Add theory for indicator function.
|
file | diff | annotate |
| Thu, 01 Jul 2010 08:12:55 +0200 |
repaired line ending
|
file | diff | annotate |
| Wed, 30 Jun 2010 17:12:38 +0200 |
one unified Word theory
|
file | diff | annotate |
| Wed, 30 Jun 2010 16:46:44 +0200 |
more speaking names
|
file | diff | annotate |
| Wed, 30 Jun 2010 16:28:14 +0200 |
more speaking theory names
|
file | diff | annotate |
| Fri, 25 Jun 2010 18:05:36 +0200 |
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 |
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 |
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
|
file | diff | annotate |
| Fri, 25 Jun 2010 16:15:03 +0200 |
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
|
file | diff | annotate |
| Thu, 24 Jun 2010 11:08:21 +0200 |
more accurate dependencies;
|
file | diff | annotate |
| Tue, 22 Jun 2010 23:54:02 +0200 |
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 |
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
|
file | diff | annotate |