src/HOL/IsaMakefile
Fri, 29 Oct 2010 18:17:08 +0200 added crafted list of SMT built-in constants
Thu, 28 Oct 2010 22:39:59 +0200 moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
Tue, 26 Oct 2010 12:17:19 +0200 reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
Tue, 26 Oct 2010 11:45:12 +0200 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
Mon, 25 Oct 2010 21:17:16 +0200 adding new predicate compiler files to the IsaMakefile
Mon, 25 Oct 2010 13:36:20 +0200 merged
Mon, 25 Oct 2010 13:34:57 +0200 moved sledgehammer to Plain; tuned dependencies
Mon, 25 Oct 2010 11:42:05 +0200 merged
Mon, 25 Oct 2010 10:30:46 +0200 introduced manual version of "Auto Solve" as "solve_direct"
Sat, 23 Oct 2010 23:42:04 +0200 integrated partial_function into HOL-Plain
Fri, 22 Oct 2010 18:38:59 +0200 splitting Hotel Key card example into specification and the two tests for counter example generation
Fri, 22 Oct 2010 13:54:51 +0200 renamed files
Tue, 05 Oct 2010 11:10:37 +0200 factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
Tue, 05 Oct 2010 10:28:11 +0200 factor out "Meson_Tactic" from "Meson_Clausify"
Mon, 04 Oct 2010 22:45:09 +0200 move Metis into Plain
Mon, 04 Oct 2010 22:01:34 +0200 added "Meson" theory to Makefile
Mon, 04 Oct 2010 21:37:42 +0200 move MESON files together
Wed, 29 Sep 2010 23:26:39 +0200 rename file
Wed, 29 Sep 2010 09:07:58 +0200 moved old_primrec source to nominal package, where it is still used
Tue, 28 Sep 2010 15:39:59 +0200 dropped old primrec package
Tue, 28 Sep 2010 12:47:55 +0200 modernized session
Mon, 27 Sep 2010 10:44:08 +0200 rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
Thu, 23 Sep 2010 14:50:18 +0200 splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
Mon, 20 Sep 2010 15:10:21 +0200 Factored out ML into separate file
Fri, 17 Sep 2010 16:38:11 +0200 merged
Thu, 16 Sep 2010 16:24:23 +0200 added new "Metis_Reconstruct" module, temporarily empty
Thu, 16 Sep 2010 16:12:02 +0200 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
Fri, 17 Sep 2010 10:52:35 +0200 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
Thu, 16 Sep 2010 11:12:08 +0200 factored out TSTP/SPASS/Vampire proof parsing;
Wed, 15 Sep 2010 20:47:14 +0200 dropped obsolete src/Tools/random_word.ML -- superseded by src/Tools/Metis/src/Random.sml stemming from the Metis distribution;
Wed, 15 Sep 2010 15:35:01 +0200 more accurate dependencies
Wed, 15 Sep 2010 13:44:10 +0200 more accurate dependencies
Mon, 13 Sep 2010 21:24:10 +0200 merged
Sat, 11 Sep 2010 10:28:44 +0200 start renaming "Auto_Counterexample" to "Auto_Tools";
Mon, 13 Sep 2010 14:54:02 +0200 print mode for Imperative HOL overview; tuned and more accurate dependencies
Fri, 10 Sep 2010 09:56:28 +0200 more correct dependencies
Wed, 08 Sep 2010 16:01:06 +0200 merge
Mon, 06 Sep 2010 17:51:26 +0200 remove "minipick" (the toy version of Nitpick) and some tests;
Tue, 07 Sep 2010 11:52:43 +0200 merged
Tue, 07 Sep 2010 11:51:53 +0200 adding the Reg_Exp example
Tue, 07 Sep 2010 11:51:53 +0200 adding IMP quickcheck examples
Tue, 07 Sep 2010 11:51:53 +0200 adding the CFG example to the build process
Tue, 07 Sep 2010 11:51:53 +0200 adding a List example (challenge from Tobias) for counterexample search
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
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);
Mon, 06 Sep 2010 13:22:11 +0200 modernized session ROOT setup;
Thu, 02 Sep 2010 17:12:16 +0200 just one refute.ML;
Thu, 02 Sep 2010 08:29:30 +0200 merged
Tue, 31 Aug 2010 23:52:59 +0200 move file
Tue, 31 Aug 2010 23:46:23 +0200 shorten a few file names
Wed, 01 Sep 2010 12:01:19 +0200 factored out generic part of Scala serializer into code_namespace.ML
Wed, 01 Sep 2010 07:53:31 +0200 merged
Tue, 31 Aug 2010 08:00:51 +0200 adding Lambda example theory; tuned
Tue, 31 Aug 2010 20:24:28 +0200 "try" -- a new diagnosis tool that tries to apply several methods in parallel
Wed, 25 Aug 2010 16:59:49 +0200 adding hotel keycard example for prolog generation
Mon, 23 Aug 2010 19:35:57 +0200 Rewrite the Probability theory.
Fri, 20 Aug 2010 17:48:30 +0200 split and enriched theory SetsAndFunctions
Wed, 18 Aug 2010 16:59:35 +0200 removed separate quickcheck_record module
Tue, 17 Aug 2010 16:44:24 +0200 dropped SML typedef_codegen: does not fit to code equations for record operations any longer
Tue, 17 Aug 2010 16:27:58 +0200 deleted typecopy package