| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
don't slice if there are too few facts
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
nicer failure message when one-line proof reconstruction fails
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
make SML/NJ happy
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
make all messages urgent in verbose mode
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
minimize automatically even if Metis failed, if the external prover was really fast
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
fixed syntax of min options
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
better merging of similar outputs
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
update minimization documentation
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
imported patch sledge_doc_metis_as_prover
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
automatically minimize with Metis when this can be done within a few seconds
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
minimize with Metis if possible
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
|
changeset |
files
|
| Mon, 30 May 2011 15:30:05 +0100 |
paulson |
Workaround for hyperref bug affecting index entries involving the | symbol
|
changeset |
files
|
| Mon, 30 May 2011 13:58:00 +0200 |
bulwahn |
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
|
changeset |
files
|
| Mon, 30 May 2011 13:57:59 +0200 |
bulwahn |
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
|
changeset |
files
|
| Mon, 30 May 2011 12:20:04 +0100 |
paulson |
merged multiple heads
|
changeset |
files
|
| Mon, 30 May 2011 12:15:17 +0100 |
paulson |
Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
|
changeset |
files
|
| Sun, 29 May 2011 19:40:56 +0200 |
blanchet |
always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
|
changeset |
files
|
| Sun, 29 May 2011 19:40:56 +0200 |
blanchet |
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
|
changeset |
files
|
| Fri, 27 May 2011 21:11:44 +0200 |
krauss |
function tutorial: do not omit termination proof, even when discussing other things
|
changeset |
files
|
| Fri, 27 May 2011 16:45:24 +0200 |
boehmes |
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
|
changeset |
files
|
| Fri, 27 May 2011 10:41:09 +0200 |
blanchet |
document new "try"
|
changeset |
files
|
| Fri, 27 May 2011 10:33:16 +0200 |
blanchet |
tuned comments
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
new timeout section (cf. Nitpick manual)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
cleanup proof text generation code
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
more Sledgehammer documentation updates
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
minor update
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
try both "metis" and (on failure) "metisFT" in replay
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
show time taken for reconstruction
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
unbreak "max_potential" logic
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
more concise output
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
compile
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
repaired theory merging and defined/used helpers
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
make Sledgehammer a little bit less verbose in "try"
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try cases gracefully in Try Methods
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try case gracefully in Solve Direct
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
update SML section of documentation
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try case gracefully in Nitpick
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try case of Sledgehammer better
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
removed FIXME: "try_methods" doesn't take a clasimpmod, because it needs to generate Isar proof text in case of success and hence needs total control over its arguments
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "Auto_Tools" "Try"
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "try" "try_methods"
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "metis_timeout" to "preplay_timeout" and continued implementation
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
minor fixes to Sledgehammer docs
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
shorten minimizer command further, exploiting until-now-undocumented syntax
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
minor tweaks to the Nitpick documentation
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
added syntax for specifying Metis timeout (currently used only by SMT solvers)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
readded Waldmeister as default to the documentation and other minor changes
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
reintroduced Waldmeister but limit the number of remote threads created
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
minor doc adjustments
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
make output more concise
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
merge timeout messages from several ATPs into one message to avoid clutter
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
mention contributions from LCP and explain metis and metisFT encodings
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fixed trivial fact detection
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
cleaner handling of equality and proxies (esp. for THF)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
recognize more ATP failures
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fully support all type system encodings in typed formats (TFF, THF)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
take out Waldmeister from default for now -- success rate too low on Judgment Day
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
document relevance filter a bit more
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
|
changeset |
files
|
| Thu, 26 May 2011 23:21:00 +0200 |
noschinl |
instance inat for complete_lattice
|
changeset |
files
|
| Thu, 26 May 2011 22:02:40 +0200 |
boehmes |
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
|
changeset |
files
|
| Thu, 26 May 2011 20:51:03 +0200 |
hoelzl |
integral strong monotone; finite subadditivity for measure
|
changeset |
files
|
| Thu, 26 May 2011 20:49:56 +0200 |
hoelzl |
composition of convex and measurable function is measurable
|
changeset |
files
|
| Thu, 26 May 2011 17:59:39 +0200 |
hoelzl |
introduce independence of two random variables
|
changeset |
files
|
| Thu, 26 May 2011 17:40:01 +0200 |
hoelzl |
add lemma indep_distribution_eq_measure
|
changeset |
files
|
| Thu, 26 May 2011 14:12:06 +0200 |
hoelzl |
add lemma indep_rv_finite
|
changeset |
files
|
| Thu, 26 May 2011 14:12:03 +0200 |
hoelzl |
generalize setsum_cases
|
changeset |
files
|
| Thu, 26 May 2011 14:12:02 +0200 |
hoelzl |
add lemma borel_0_1_law
|
changeset |
files
|
| Thu, 26 May 2011 14:12:01 +0200 |
hoelzl |
add lemma sigma_sets_singleton
|
changeset |
files
|
| Thu, 26 May 2011 14:12:00 +0200 |
hoelzl |
use abbrevitation events == sets M
|
changeset |
files
|
| Thu, 26 May 2011 14:11:58 +0200 |
hoelzl |
add lemma kolmogorov_0_1_law
|
changeset |
files
|
| Thu, 26 May 2011 14:11:57 +0200 |
hoelzl |
add lemma indep_sets_collect_sigma
|
changeset |
files
|
| Thu, 26 May 2011 09:42:04 +0200 |
bulwahn |
improving code_int setup in Quickcheck_Narrowing; adding partial_term_of class in Quickcheck_Narrowing
|
changeset |
files
|
| Thu, 26 May 2011 09:42:02 +0200 |
bulwahn |
extending terms of Code_Evaluation by Free to allow partial terms
|
changeset |
files
|
| Thu, 26 May 2011 00:20:28 +0200 |
krauss |
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
|
changeset |
files
|
| Thu, 26 May 2011 00:12:30 +0200 |
krauss |
css rules for highlighting sendback text
|
changeset |
files
|
| Thu, 26 May 2011 00:12:01 +0200 |
krauss |
invert event propagation flag -- in lobobrowser api, true means re-propagate
|
changeset |
files
|
| Wed, 25 May 2011 08:31:36 +0200 |
blanchet |
eta-expand to make SML/NJ happy
|
changeset |
files
|
| Tue, 24 May 2011 18:04:23 +0200 |
blanchet |
ensure that the argument of logical negation is enclosed in parentheses in THF mode
|
changeset |
files
|
| Tue, 24 May 2011 17:05:29 +0200 |
blanchet |
hack to obtain potable step names from Waldmeister
|
changeset |
files
|
| Tue, 24 May 2011 17:04:35 +0200 |
blanchet |
respect user's intention better when setting the CNF_UEQ type system (esp. w.r.t. "erased")
|
changeset |
files
|
| Tue, 24 May 2011 13:29:32 +0200 |
blanchet |
further reduce the number of facts passed to less used remote ATPs
|
changeset |
files
|
| Tue, 24 May 2011 11:55:59 +0200 |
blanchet |
added quietness flag
|
changeset |
files
|
| Tue, 24 May 2011 10:03:15 +0200 |
blanchet |
pass fewer relevant facts to less used remote systems
|
changeset |
files
|
| Tue, 24 May 2011 10:01:03 +0200 |
blanchet |
more work on parsing LEO-II proofs and extracting uses of extensionality
|
changeset |
files
|
| Tue, 24 May 2011 10:01:00 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 24 May 2011 10:00:38 +0200 |
blanchet |
more work on parsing LEO-II proofs without lambdas
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
slightly gracefuller handling of LEO-II and Satallax output
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
document primitive support for LEO-II and Satallax
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
identify HOL functions with THF functions
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
started adding support for THF output (but no lambdas)
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
eliminated more code duplication in Nitrox
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
reduce code duplication in Nitrox
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
use \<emdash> rather than \<midarrow>
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
fixed de Bruijn index bug
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
clearer SystemOnTPTP errors
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
give fewer equations to Waldmeister
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
detect inappropriate problems and crashes better in Waldmeister
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
tuning -- the "appropriate" terminology is inspired from TPTP
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
|
changeset |
files
|
| Mon, 23 May 2011 19:21:05 +0200 |
hoelzl |
move lemmas to Extended_Reals and Extended_Real_Limits
|
changeset |
files
|
| Mon, 23 May 2011 10:58:21 +0200 |
krauss |
separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
|
changeset |
files
|
| Sun, 22 May 2011 22:22:25 +0200 |
krauss |
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
|
changeset |
files
|
| Sun, 22 May 2011 20:59:13 +0200 |
krauss |
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
|
changeset |
files
|
| Sun, 22 May 2011 14:51:42 +0200 |
blanchet |
added message when Waldmeister isn't run
|
changeset |
files
|
| Sun, 22 May 2011 14:51:42 +0200 |
blanchet |
slightly improved documentation
|
changeset |
files
|
| Sun, 22 May 2011 14:51:42 +0200 |
blanchet |
improved Waldmeister support -- even run it by default on unit equational goals
|
changeset |
files
|
| Sun, 22 May 2011 14:51:41 +0200 |
blanchet |
fish out axioms in Waldmeister output
|
changeset |
files
|
| Sun, 22 May 2011 14:51:04 +0200 |
blanchet |
removed SNARK hack now that SNARK is fixed
|
changeset |
files
|
| Sun, 22 May 2011 14:51:04 +0200 |
blanchet |
recognize one more SystemOnTPTP error
|
changeset |
files
|
| Sun, 22 May 2011 14:51:04 +0200 |
blanchet |
document Waldmeister
|
changeset |
files
|
| Sun, 22 May 2011 14:51:01 +0200 |
blanchet |
added support for remote Waldmeister
|
changeset |
files
|
| Sun, 22 May 2011 14:50:32 +0200 |
blanchet |
added Waldmeister
|
changeset |
files
|
| Sun, 22 May 2011 14:49:35 +0200 |
blanchet |
reorganized ATP formats a little bit
|
changeset |
files
|
| Mon, 06 Jun 2011 22:02:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 06 Jun 2011 19:13:48 +0200 |
wenzelm |
removed odd remains of low-level session management;
|
changeset |
files
|
| Mon, 06 Jun 2011 19:08:46 +0200 |
wenzelm |
moved incr_boundvars;
|
changeset |
files
|
| Mon, 06 Jun 2011 18:05:38 +0200 |
wenzelm |
modernized and re-unified Thm.transfer;
|
changeset |
files
|
| Mon, 06 Jun 2011 17:51:14 +0200 |
wenzelm |
removed obsolete material (superseded by implementation manual);
|
changeset |
files
|
| Sun, 05 Jun 2011 22:09:04 +0200 |
wenzelm |
removed somewhat low-level stuff (cf. attribute "swapped" in isar-ref);
|
changeset |
files
|
| Sun, 05 Jun 2011 22:02:54 +0200 |
wenzelm |
updated and re-unified classical proof methods;
|
changeset |
files
|
| Sun, 05 Jun 2011 20:23:05 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 05 Jun 2011 20:15:47 +0200 |
wenzelm |
updated and re-unified classical rule declarations;
|
changeset |
files
|
| Sat, 04 Jun 2011 22:09:42 +0200 |
wenzelm |
moved/updated introduction to Classical Reasoner;
|
changeset |
files
|
| Sat, 04 Jun 2011 19:39:45 +0200 |
wenzelm |
tuned secref (still dangling);
|
changeset |
files
|
| Fri, 03 Jun 2011 22:39:23 +0200 |
wenzelm |
updated and re-unified material on simprocs;
|
changeset |
files
|
| Fri, 03 Jun 2011 21:32:48 +0200 |
wenzelm |
removed some old stuff;
|
changeset |
files
|
| Thu, 02 Jun 2011 14:11:24 +0200 |
wenzelm |
tuned headings;
|
changeset |
files
|
| Thu, 02 Jun 2011 14:08:46 +0200 |
wenzelm |
some material on "Generalized elimination and cases";
|
changeset |
files
|
| Thu, 02 Jun 2011 13:59:23 +0200 |
wenzelm |
some material on "Structured induction proofs";
|
changeset |
files
|
| Wed, 01 Jun 2011 13:06:45 +0200 |
wenzelm |
some material on "Structured Natural Deduction";
|
changeset |
files
|
| Wed, 01 Jun 2011 12:39:04 +0200 |
wenzelm |
some material on "Calculational reasoning";
|
changeset |
files
|
| Wed, 01 Jun 2011 12:20:48 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 31 May 2011 22:47:18 +0200 |
wenzelm |
added Synopsis, with some "Notepad" material;
|
changeset |
files
|
| Tue, 31 May 2011 22:18:37 +0200 |
wenzelm |
more accurate deps;
|
changeset |
files
|
| Tue, 31 May 2011 22:15:39 +0200 |
wenzelm |
turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
|
changeset |
files
|
| Thu, 26 May 2011 22:42:52 +0200 |
wenzelm |
moved/updated basic HOL overview;
|
changeset |
files
|
| Thu, 26 May 2011 21:39:02 +0200 |
wenzelm |
updated and re-unified (co)inductive definitions in HOL;
|
changeset |
files
|
| Thu, 26 May 2011 15:56:39 +0200 |
wenzelm |
clarified current 'primrec' vs. old 'recdef';
|
changeset |
files
|
| Thu, 26 May 2011 14:24:26 +0200 |
wenzelm |
record examples;
|
changeset |
files
|
| Thu, 26 May 2011 14:12:14 +0200 |
wenzelm |
updated and simplified HOL datatype examples (NB: special treatment of distinctness has been discontinued in the vicinity of 542b34b178ec);
|
changeset |
files
|
| Thu, 26 May 2011 13:37:11 +0200 |
wenzelm |
updated and re-unified HOL rep_datatype;
|
changeset |
files
|
| Wed, 25 May 2011 22:21:38 +0200 |
wenzelm |
rearranged some sections;
|
changeset |
files
|
| Wed, 25 May 2011 22:12:46 +0200 |
wenzelm |
updated and re-unified HOL typedef, with some live examples;
|
changeset |
files
|
| Sat, 21 May 2011 11:31:59 +0200 |
wenzelm |
optional jedit_build/etc/user-settings enable to override defaults produced by late component initialization;
|
changeset |
files
|
| Sat, 21 May 2011 00:09:18 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 20 May 2011 21:38:32 +0200 |
hoelzl |
add divide_.._cancel, inverse_.._iff
|
changeset |
files
|
| Fri, 20 May 2011 21:38:32 +0200 |
hoelzl |
add surj_vimage_empty
|
changeset |
files
|
| Fri, 20 May 2011 21:38:32 +0200 |
hoelzl |
Add restricted borel measure to {0 .. 1}
|
changeset |
files
|
| Fri, 20 May 2011 21:38:32 +0200 |
hoelzl |
equations for subsets of atLeastAtMost
|
changeset |
files
|
| Sat, 21 May 2011 00:01:15 +0200 |
wenzelm |
build and run Isabelle/jEdit on the spot -- requires auxiliary "jedit_build" component;
|
changeset |
files
|
| Sat, 21 May 2011 00:00:14 +0200 |
wenzelm |
misc tuning and update;
|
changeset |
files
|
| Fri, 20 May 2011 23:59:46 +0200 |
wenzelm |
updated versions;
|
changeset |
files
|
| Fri, 20 May 2011 20:44:03 +0200 |
wenzelm |
added Isabelle_Process.is_active;
|
changeset |
files
|
| Fri, 20 May 2011 18:12:12 +0200 |
blanchet |
update example
|
changeset |
files
|
| Fri, 20 May 2011 18:01:46 +0200 |
blanchet |
name tuning
|
changeset |
files
|
| Fri, 20 May 2011 17:16:13 +0200 |
blanchet |
further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged
|
changeset |
files
|
| Fri, 20 May 2011 17:16:13 +0200 |
blanchet |
prevent unsound combinator proofs in partially typed polymorphic type systems
|
changeset |
files
|
| Fri, 20 May 2011 16:23:03 +0200 |
hoelzl |
add lemma prob_finite_product
|
changeset |
files
|
| Fri, 20 May 2011 16:22:24 +0200 |
hoelzl |
simp rules for empty intervals on dense linear order
|
changeset |
files
|
| Fri, 20 May 2011 14:12:59 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 20 May 2011 12:59:33 +0200 |
blanchet |
exercise more type systems (but only sound or quasi-sound ones)
|
changeset |
files
|
| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
added see also
|
changeset |
files
|
| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
document new type system and soundness properties of the different systems
|
changeset |
files
|
| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
|
changeset |
files
|
| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
reintroduced type encodings "poly_preds_{bang,query}", but this time being more liberal about type variables of known safe sorts
|
changeset |
files
|
| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
more doc fiddling
|
changeset |
files
|
| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
more FAQs
|
changeset |
files
|
| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
make sure the Vampire incomplete proof detection code kicks in
|
changeset |
files
|
| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
automatically use "metisFT" when typed helpers are necessary
|
changeset |
files
|
| Fri, 20 May 2011 12:47:58 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 20 May 2011 12:47:58 +0200 |
blanchet |
generate useful information for type axioms
|
changeset |
files
|
| Fri, 20 May 2011 12:47:58 +0200 |
blanchet |
slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
|
changeset |
files
|
| Fri, 20 May 2011 12:47:58 +0200 |
blanchet |
updated FAQ
|
changeset |
files
|
| Fri, 20 May 2011 12:47:58 +0200 |
blanchet |
more informative message when Sledgehammer finds an unsound proof
|
changeset |
files
|
| Fri, 20 May 2011 12:35:44 +0200 |
haftmann |
tuned proofs
|
changeset |
files
|
| Fri, 20 May 2011 12:09:54 +0200 |
haftmann |
NEWS
|
changeset |
files
|
| Fri, 20 May 2011 12:07:17 +0200 |
haftmann |
point-free characterization of operations on finite sets
|
changeset |
files
|
| Fri, 20 May 2011 11:44:34 +0200 |
haftmann |
merged
|
changeset |
files
|