Thu, 09 Jun 2011 00:16:28 +0200 be a bit more liberal with respect to the universal sort -- it sometimes help
blanchet [Thu, 09 Jun 2011 00:16:28 +0200] rev 43299
be a bit more liberal with respect to the universal sort -- it sometimes help
Thu, 09 Jun 2011 00:16:28 +0200 renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
blanchet [Thu, 09 Jun 2011 00:16:28 +0200] rev 43298
renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
Wed, 08 Jun 2011 22:13:49 +0200 merged
wenzelm [Wed, 08 Jun 2011 22:13:49 +0200] rev 43297
merged
Wed, 08 Jun 2011 17:01:07 +0200 avoid duplicate facts, which confuse the minimizer output
blanchet [Wed, 08 Jun 2011 17:01:07 +0200] rev 43296
avoid duplicate facts, which confuse the minimizer output
Wed, 08 Jun 2011 16:20:19 +0200 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
blanchet [Wed, 08 Jun 2011 16:20:19 +0200] rev 43295
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 restore comment about subtle issue
blanchet [Wed, 08 Jun 2011 16:20:18 +0200] rev 43294
restore comment about subtle issue
Wed, 08 Jun 2011 16:20:18 +0200 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
blanchet [Wed, 08 Jun 2011 16:20:18 +0200] rev 43293
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 don't launch the automatic minimizer for zero facts
blanchet [Wed, 08 Jun 2011 16:20:18 +0200] rev 43292
don't launch the automatic minimizer for zero facts
Wed, 08 Jun 2011 16:20:18 +0200 don't generate unsound proof error for missing proofs
blanchet [Wed, 08 Jun 2011 16:20:18 +0200] rev 43291
don't generate unsound proof error for missing proofs
Wed, 08 Jun 2011 16:20:18 +0200 renamed option to avoid talking about seconds, since this is now the default Isabelle unit
blanchet [Wed, 08 Jun 2011 16:20:18 +0200] rev 43290
renamed option to avoid talking about seconds, since this is now the default Isabelle unit
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip