| Wed, 17 Nov 2010 11:09:18 +0100 |
haftmann |
module for functorial mappers
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 12:13:44 +0100 |
boehmes |
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 09:25:43 +0100 |
bulwahn |
adding code and theory for smallvalue generators, but do not setup the interpretation yet
|
file |
diff |
annotate
|
| Thu, 04 Nov 2010 13:37:11 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 12:20:33 +0100 |
haftmann |
moved theory Quicksort from Library/ to ex/
|
file |
diff |
annotate
|
| Thu, 04 Nov 2010 09:53:23 +0100 |
blanchet |
moved file in makefile to reflect actual dependencies
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 21:34:07 +0200 |
wenzelm |
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:08 +0200 |
boehmes |
added crafted list of SMT built-in constants
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 22:39:59 +0200 |
wenzelm |
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 12:17:19 +0200 |
blanchet |
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
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 11:45:12 +0200 |
boehmes |
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
|
file |
diff |
annotate
|
| 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
|