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
Wed, 08 Jun 2011 16:20:18 +0200 blanchet restore comment about subtle issue
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
Wed, 08 Jun 2011 16:20:18 +0200 blanchet don't launch the automatic minimizer for zero facts
Wed, 08 Jun 2011 16:20:18 +0200 blanchet don't generate unsound proof error for missing proofs
Wed, 08 Jun 2011 16:20:18 +0200 blanchet renamed option to avoid talking about seconds, since this is now the default Isabelle unit
Wed, 08 Jun 2011 16:20:18 +0200 blanchet fixed format selection logic for Waldmeister
Wed, 08 Jun 2011 16:20:18 +0200 blanchet better default type system for Waldmeister, with fewer predicates (for types or type classes)
Wed, 08 Jun 2011 22:06:05 +0200 wenzelm simplified directory structure;
Wed, 08 Jun 2011 21:40:54 +0200 wenzelm simplified directory structure;
Wed, 08 Jun 2011 21:29:49 +0200 wenzelm further jedit build option;
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);
Wed, 08 Jun 2011 17:49:01 +0200 wenzelm updated headers;
Wed, 08 Jun 2011 17:42:07 +0200 wenzelm moved sources -- eliminated Netbeans artifact of jedit package directory;
Wed, 08 Jun 2011 17:32:31 +0200 wenzelm removed obsolete Netbeans project setup;
(0) -30000 -10000 -3000 -1000 -300 -100 -15 +15 +100 +300 +1000 +3000 +10000 +30000 tip