| 2010-12-01 |
wenzelm |
activate subtyping/coercions in theory Complex_Main;
|
file |
diff |
annotate
|
| 2010-12-01 |
wenzelm |
more precise dependencies;
|
file |
diff |
annotate
|
| 2010-11-28 |
huffman |
fix cut-and-paste errors for HOLCF entries in IsaMakefile
|
file |
diff |
annotate
|
| 2010-11-28 |
huffman |
moved directory src/HOLCF to src/HOL/HOLCF;
|
file |
diff |
annotate
|
| 2010-11-23 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2010-11-22 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2010-11-22 |
haftmann |
replaced misleading Fset/fset name -- these do not stand for finite sets
|
file |
diff |
annotate
|
| 2010-11-22 |
boehmes |
added prove reconstruction for injective functions;
|
file |
diff |
annotate
|
| 2010-11-22 |
bulwahn |
adding Enum to HOL-Main image and removing it from HOL-Library
|
file |
diff |
annotate
|
| 2010-11-22 |
bulwahn |
adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test
|
file |
diff |
annotate
|
| 2010-11-22 |
bulwahn |
adding birthday paradoxon from some abandoned drawer
|
file |
diff |
annotate
|
| 2010-11-17 |
haftmann |
module for functorial mappers
|
file |
diff |
annotate
|
| 2010-11-08 |
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
|
| 2010-11-08 |
bulwahn |
adding code and theory for smallvalue generators, but do not setup the interpretation yet
|
file |
diff |
annotate
|
| 2010-11-04 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2010-11-03 |
haftmann |
moved theory Quicksort from Library/ to ex/
|
file |
diff |
annotate
|
| 2010-11-04 |
blanchet |
moved file in makefile to reflect actual dependencies
|
file |
diff |
annotate
|
| 2010-10-29 |
wenzelm |
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
|
file |
diff |
annotate
|
| 2010-10-29 |
boehmes |
added crafted list of SMT built-in constants
|
file |
diff |
annotate
|
| 2010-10-28 |
wenzelm |
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
|
file |
diff |
annotate
|
| 2010-10-26 |
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
|
| 2010-10-26 |
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
|
| 2010-10-25 |
bulwahn |
adding new predicate compiler files to the IsaMakefile
|
file |
diff |
annotate
|
| 2010-10-25 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2010-10-25 |
haftmann |
moved sledgehammer to Plain; tuned dependencies
|
file |
diff |
annotate
|
| 2010-10-25 |
blanchet |
merged
|
file |
diff |
annotate
|
| 2010-10-25 |
blanchet |
introduced manual version of "Auto Solve" as "solve_direct"
|
file |
diff |
annotate
|
| 2010-10-23 |
krauss |
integrated partial_function into HOL-Plain
|
file |
diff |
annotate
|
| 2010-10-22 |
bulwahn |
splitting Hotel Key card example into specification and the two tests for counter example generation
|
file |
diff |
annotate
|
| 2010-10-22 |
blanchet |
renamed files
|
file |
diff |
annotate
|
| 2010-10-05 |
blanchet |
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
|
file |
diff |
annotate
|
| 2010-10-05 |
blanchet |
factor out "Meson_Tactic" from "Meson_Clausify"
|
file |
diff |
annotate
|
| 2010-10-04 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
|
| 2010-10-04 |
blanchet |
added "Meson" theory to Makefile
|
file |
diff |
annotate
|
| 2010-10-04 |
blanchet |
move MESON files together
|
file |
diff |
annotate
|
| 2010-09-29 |
blanchet |
rename file
|
file |
diff |
annotate
|
| 2010-09-29 |
haftmann |
moved old_primrec source to nominal package, where it is still used
|
file |
diff |
annotate
|
| 2010-09-28 |
haftmann |
dropped old primrec package
|
file |
diff |
annotate
|
| 2010-09-28 |
haftmann |
modernized session
|
file |
diff |
annotate
|
| 2010-09-27 |
blanchet |
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
|
file |
diff |
annotate
|
| 2010-09-23 |
bulwahn |
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
|
file |
diff |
annotate
|
| 2010-09-20 |
haftmann |
Factored out ML into separate file
|
file |
diff |
annotate
|
| 2010-09-17 |
blanchet |
merged
|
file |
diff |
annotate
|
| 2010-09-16 |
blanchet |
added new "Metis_Reconstruct" module, temporarily empty
|
file |
diff |
annotate
|
| 2010-09-16 |
blanchet |
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
|
file |
diff |
annotate
|
| 2010-09-17 |
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
|
| 2010-09-16 |
blanchet |
factored out TSTP/SPASS/Vampire proof parsing;
|
file |
diff |
annotate
|
| 2010-09-15 |
wenzelm |
dropped obsolete src/Tools/random_word.ML -- superseded by src/Tools/Metis/src/Random.sml stemming from the Metis distribution;
|
file |
diff |
annotate
|
| 2010-09-15 |
haftmann |
more accurate dependencies
|
file |
diff |
annotate
|
| 2010-09-15 |
haftmann |
more accurate dependencies
|
file |
diff |
annotate
|
| 2010-09-13 |
blanchet |
merged
|
file |
diff |
annotate
|
| 2010-09-11 |
blanchet |
start renaming "Auto_Counterexample" to "Auto_Tools";
|
file |
diff |
annotate
|
| 2010-09-13 |
haftmann |
print mode for Imperative HOL overview; tuned and more accurate dependencies
|
file |
diff |
annotate
|
| 2010-09-10 |
haftmann |
more correct dependencies
|
file |
diff |
annotate
|
| 2010-09-08 |
blanchet |
merge
|
file |
diff |
annotate
|
| 2010-09-06 |
blanchet |
remove "minipick" (the toy version of Nitpick) and some tests;
|
file |
diff |
annotate
|
| 2010-09-07 |
bulwahn |
merged
|
file |
diff |
annotate
|
| 2010-09-07 |
bulwahn |
adding the Reg_Exp example
|
file |
diff |
annotate
|
| 2010-09-07 |
bulwahn |
adding IMP quickcheck examples
|
file |
diff |
annotate
|
| 2010-09-07 |
bulwahn |
adding the CFG example to the build process
|
file |
diff |
annotate
|