| Thu, 09 Jun 2011 08:32:16 +0200 |
bulwahn |
adding theory Quickcheck_Narrowing to HOL-Main image
|
changeset |
files
|
| Thu, 09 Jun 2011 08:32:15 +0200 |
bulwahn |
adapting IsaMakefile
|
changeset |
files
|
| Thu, 09 Jun 2011 08:32:14 +0200 |
bulwahn |
moving Quickcheck_Narrowing from Library to base directory
|
changeset |
files
|
| Thu, 09 Jun 2011 08:32:13 +0200 |
bulwahn |
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
|
changeset |
files
|
| Thu, 09 Jun 2011 08:31:41 +0200 |
bulwahn |
local simp rule in List_Cset
|
changeset |
files
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
compile
|
changeset |
files
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
|
changeset |
files
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
added a really fully typed translation as a fallback for Metis, in rare cases where Metis correctly proves a theorem but has type-unsound steps in it (which is likelier to happen with some of the lighter translations)
|
changeset |
files
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
improve sort inference in Metis proofs -- in some rare cases Metis steals Isabelle's variable names and the sorts must then be inferred as well
|
changeset |
files
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
removed needless function that duplicated standard functionality, with a little unnecessary twist
|
changeset |
files
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
removed more dead code
|
changeset |
files
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
be a bit more liberal with respect to the universal sort -- it sometimes help
|
changeset |
files
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
|
changeset |
files
|
| Wed, 08 Jun 2011 22:13:49 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 08 Jun 2011 22:06:05 +0200 |
wenzelm |
simplified directory structure;
|
changeset |
files
|
| Wed, 08 Jun 2011 21:40:54 +0200 |
wenzelm |
simplified directory structure;
|
changeset |
files
|
| Wed, 08 Jun 2011 21:29:49 +0200 |
wenzelm |
further jedit build option;
|
changeset |
files
|
| Wed, 08 Jun 2011 20:58:51 +0200 |
wenzelm |
build jedit as part of regular startup script (in that case depending on jedit_build component);
|
changeset |
files
|
| Wed, 08 Jun 2011 17:49:01 +0200 |
wenzelm |
updated headers;
|
changeset |
files
|
| Wed, 08 Jun 2011 17:42:07 +0200 |
wenzelm |
moved sources -- eliminated Netbeans artifact of jedit package directory;
|
changeset |
files
|
| Wed, 08 Jun 2011 17:32:31 +0200 |
wenzelm |
removed obsolete Netbeans project setup;
|
changeset |
files
|
| Wed, 08 Jun 2011 17:11:00 +0200 |
wenzelm |
support fresh build of jars;
|
changeset |
files
|
| Wed, 08 Jun 2011 16:19:22 +0200 |
wenzelm |
more jvmpath wrapping for Cygwin;
|
changeset |
files
|
| Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
changeset |
files
|
| Wed, 08 Jun 2011 15:39:55 +0200 |
wenzelm |
pervasive Output operations;
|
changeset |
files
|
| Wed, 08 Jun 2011 15:25:44 +0200 |
wenzelm |
modernized Proof_Context;
|
changeset |
files
|
| Wed, 08 Jun 2011 14:44:54 +0200 |
wenzelm |
standardized header;
|
changeset |
files
|
| Wed, 08 Jun 2011 17:01:07 +0200 |
blanchet |
avoid duplicate facts, which confuse the minimizer output
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:19 +0200 |
blanchet |
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
restore comment about subtle issue
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
don't launch the automatic minimizer for zero facts
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
don't generate unsound proof error for missing proofs
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
renamed option to avoid talking about seconds, since this is now the default Isabelle unit
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
fixed format selection logic for Waldmeister
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
better default type system for Waldmeister, with fewer predicates (for types or type classes)
|
changeset |
files
|
| Wed, 08 Jun 2011 13:45:01 +0200 |
boehmes |
merged
|
changeset |
files
|
| Wed, 08 Jun 2011 13:43:15 +0200 |
boehmes |
updated SMT certificates
|
changeset |
files
|
| Wed, 08 Jun 2011 11:59:45 +0200 |
boehmes |
only collect substituions neither seen before nor derived in the same refinement step
|
changeset |
files
|
| Wed, 08 Jun 2011 12:13:37 +0200 |
wenzelm |
updated imports (cf. 93b1183e43e5);
|
changeset |
files
|
| Wed, 08 Jun 2011 10:24:07 +0200 |
wenzelm |
merged
|
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
|