src/HOL/IsaMakefile
Tue, 07 Sep 2010 11:51:53 +0200 bulwahn adding the Reg_Exp example
Tue, 07 Sep 2010 11:51:53 +0200 bulwahn adding IMP quickcheck examples
Tue, 07 Sep 2010 11:51:53 +0200 bulwahn adding the CFG example to the build process
Tue, 07 Sep 2010 11:51:53 +0200 bulwahn adding a List example (challenge from Tobias) for counterexample search
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
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);
Mon, 06 Sep 2010 13:22:11 +0200 wenzelm modernized session ROOT setup;
Thu, 02 Sep 2010 17:12:16 +0200 wenzelm just one refute.ML;
Thu, 02 Sep 2010 08:29:30 +0200 blanchet merged
Tue, 31 Aug 2010 23:52:59 +0200 blanchet move file
Tue, 31 Aug 2010 23:46:23 +0200 blanchet shorten a few file names
Wed, 01 Sep 2010 12:01:19 +0200 haftmann factored out generic part of Scala serializer into code_namespace.ML
Wed, 01 Sep 2010 07:53:31 +0200 bulwahn merged
Tue, 31 Aug 2010 08:00:51 +0200 bulwahn adding Lambda example theory; tuned
Tue, 31 Aug 2010 20:24:28 +0200 blanchet "try" -- a new diagnosis tool that tries to apply several methods in parallel
Wed, 25 Aug 2010 16:59:49 +0200 bulwahn adding hotel keycard example for prolog generation
Mon, 23 Aug 2010 19:35:57 +0200 hoelzl Rewrite the Probability theory.
Fri, 20 Aug 2010 17:48:30 +0200 haftmann split and enriched theory SetsAndFunctions
Wed, 18 Aug 2010 16:59:35 +0200 haftmann removed separate quickcheck_record module
Tue, 17 Aug 2010 16:44:24 +0200 haftmann dropped SML typedef_codegen: does not fit to code equations for record operations any longer
Tue, 17 Aug 2010 16:27:58 +0200 haftmann deleted typecopy package
Thu, 12 Aug 2010 17:56:43 +0200 haftmann moved Record.thy from session Plain to Main; avoid variable name acc
Mon, 09 Aug 2010 12:05:48 +0200 blanchet move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
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);
Sun, 01 Aug 2010 10:15:44 +0200 bulwahn adding Code_Prolog theory to IsaMakefile and HOL-Library root file
Thu, 29 Jul 2010 17:27:54 +0200 bulwahn adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
Wed, 28 Jul 2010 19:04:59 +0200 blanchet consequence of directory renaming
Tue, 27 Jul 2010 17:56:01 +0200 blanchet rename "ATP_Manager" ML module to "Sledgehammer";
Tue, 27 Jul 2010 17:43:11 +0200 blanchet complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
Mon, 26 Jul 2010 11:10:35 +0200 haftmann added Code_Natural.thy
Wed, 21 Jul 2010 18:13:15 +0200 bulwahn merged
Wed, 21 Jul 2010 18:11:51 +0200 bulwahn added new theories to IsaMakefile and ROOT.ML
Wed, 21 Jul 2010 16:50:42 +0200 wenzelm merged
Mon, 19 Jul 2010 16:09:43 +0200 haftmann discontinued pretending that abel_cancel is logic-independent; cleaned up junk
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;
Wed, 14 Jul 2010 14:16:12 +0200 haftmann load cache_io before code generator; moved adhoc-overloading to generic tools
Tue, 13 Jul 2010 00:15:37 +0200 krauss uniform do notation for monads
Tue, 13 Jul 2010 00:15:37 +0200 krauss generic ad-hoc overloading via check/uncheck
Mon, 12 Jul 2010 21:38:37 +0200 wenzelm moved misc legacy stuff from OldGoals to Misc_Legacy;
Mon, 12 Jul 2010 20:35:10 +0200 wenzelm removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years;
Mon, 12 Jul 2010 16:40:48 +0200 haftmann dropped empty theory
Mon, 12 Jul 2010 16:19:15 +0200 haftmann split off mrec into separate theory
Mon, 12 Jul 2010 08:58:27 +0200 haftmann merged
Mon, 12 Jul 2010 08:58:12 +0200 haftmann more regular session structure
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;
Fri, 09 Jul 2010 17:15:03 +0200 krauss moved example to its own file in HOL/ex
Thu, 08 Jul 2010 16:28:18 +0200 haftmann more accurate dependencies
Thu, 08 Jul 2010 16:17:44 +0200 haftmann tuned tabs
Fri, 02 Jul 2010 14:23:16 +0200 haftmann build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
Thu, 01 Jul 2010 19:14:54 +0200 wenzelm avoid Old_Number_Theory;
Thu, 01 Jul 2010 11:48:42 +0200 hoelzl Add theory for indicator function.
Thu, 01 Jul 2010 08:12:55 +0200 haftmann repaired line ending
Wed, 30 Jun 2010 17:12:38 +0200 haftmann one unified Word theory
Wed, 30 Jun 2010 16:46:44 +0200 haftmann more speaking names
Wed, 30 Jun 2010 16:28:14 +0200 haftmann more speaking theory names
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
Fri, 25 Jun 2010 17:08:39 +0200 blanchet renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
Fri, 25 Jun 2010 16:42:06 +0200 blanchet merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
Fri, 25 Jun 2010 16:15:03 +0200 blanchet renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
Thu, 24 Jun 2010 11:08:21 +0200 wenzelm more accurate dependencies;
less more (0) -1000 -300 -100 -60 tip