src/HOL/ex/atp_export.ML
Wed, 08 Jun 2011 08:47:43 +0200 blanchet killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
Tue, 07 Jun 2011 14:17:35 +0200 blanchet optimized the relevance filter a little bit
Tue, 07 Jun 2011 07:06:24 +0200 blanchet renamed ML function
Tue, 07 Jun 2011 07:04:53 +0200 blanchet renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
less more (0) tip