src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
Wed, 18 Jul 2012 08:44:04 +0200 implemented meshing of Iter and MaSh results
Wed, 18 Jul 2012 08:44:04 +0200 implemented MaSh QUERY operation
Wed, 18 Jul 2012 08:44:04 +0200 implemented low-level MaSh ADD operation
Wed, 18 Jul 2012 08:44:04 +0200 make tracing an option
Wed, 18 Jul 2012 08:44:04 +0200 better zipping of MaSh facts
Wed, 18 Jul 2012 08:44:04 +0200 implemented MaSh learn theory function
Wed, 18 Jul 2012 08:44:04 +0200 more work on MaSh
Wed, 18 Jul 2012 08:44:04 +0200 improved MaSh string escaping and make more operations string-based
Wed, 18 Jul 2012 08:44:03 +0200 more implementation work on MaSh
Wed, 18 Jul 2012 08:44:03 +0200 started implementing MaSh client-side I/O
Wed, 18 Jul 2012 08:44:03 +0200 centrally construct expensive data structures
Wed, 18 Jul 2012 08:44:03 +0200 more work on MaSh
Wed, 18 Jul 2012 08:44:03 +0200 compile
Wed, 18 Jul 2012 08:44:03 +0200 gracefully handle the case of empty theories when going up the accessibility chain
Wed, 18 Jul 2012 08:44:03 +0200 renamed Sledgehammer options
Wed, 18 Jul 2012 08:44:03 +0200 more code rationalization in relevance filter
Wed, 18 Jul 2012 08:44:03 +0200 systematize lazy names in relevance filter
Wed, 18 Jul 2012 08:44:03 +0200 rationalize relevance filter, slowing moving code from Iter to MaSh
Wed, 11 Jul 2012 21:43:19 +0200 moved most of MaSh exporter code to Sledgehammer
Wed, 11 Jul 2012 21:43:19 +0200 dummy implementation
Wed, 11 Jul 2012 21:43:19 +0200 split relevance filter code into three files