src/HOL/TPTP/atp_theory_export.ML
2016-03-07 wenzelm 2016-03-07 File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output; clarified treatment of whitespace in some bash scripts;
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2015-12-19 blanchet 2015-12-19 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
2015-10-05 blanchet 2015-10-05 extended theory exporter to also export MePo-selected facts
2015-08-13 wenzelm 2015-08-13 tuned signature, in accordance to sortBy in Scala;
2015-07-03 wenzelm 2015-07-03 clarified context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-03-03 blanchet 2015-03-03 SPASS-Pirate is now called Pirate
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-06 wenzelm 2014-11-06 proper Keyword.keywords (cf. 82a71046dce8);
2014-07-25 blanchet 2014-07-25 compile
2014-06-24 blanchet 2014-06-24 tuning
2014-06-24 blanchet 2014-06-24 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
2014-06-16 blanchet 2014-06-16 compile
2013-12-17 blanchet 2013-12-17 primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
2013-10-24 blanchet 2013-10-24 use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
2013-09-29 wenzelm 2013-09-29 made SML/NJ happy (NB: toplevel ML environment is unmanaged);
2013-09-12 blanchet 2013-09-12 prefixed types and some functions with "atp_" for disambiguation
2013-08-13 blanchet 2013-08-13 Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)
2013-07-29 blanchet 2013-07-29 added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-05-15 blanchet 2013-05-15 renamed Sledgehammer functions with 'for' in their names to 'of'
2013-04-09 blanchet 2013-04-09 handle case clashes on Mac file system by encoding goal numbers
2013-04-09 blanchet 2013-04-09 smoothly handle cyclic graphs
2013-04-09 blanchet 2013-04-09 compile + fixed naming convention
2013-04-09 blanchet 2013-04-09 no need to filter tautologies anymore -- they are prefiltered by "all_facts"'
2013-04-09 blanchet 2013-04-09 work on CASC LTB ISA exporter
2013-04-08 blanchet 2013-04-08 try to preserve original linearization
2013-04-08 blanchet 2013-04-08 use somewhat lighter encoding
2013-01-17 blanchet 2013-01-17 added E-Par support
2013-01-04 blanchet 2013-01-04 refined class handling, to prevent cycles in fact graph
2012-12-13 blanchet 2012-12-13 generate comments with original names for debugging
2012-12-12 blanchet 2012-12-12 merge aliased theorems in MaSh dependencies, modulo symmetry of equality
2012-12-08 blanchet 2012-12-08 don't blacklist "case" theorems -- this causes problems in MaSh later
2012-08-07 blanchet 2012-08-07 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
2012-07-26 blanchet 2012-07-26 repaired accessibility chains generated by MaSh exporter + tuned one function out
2012-07-23 blanchet 2012-07-23 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
2012-07-20 blanchet 2012-07-20 honor suggested MaSh weights
2012-07-20 blanchet 2012-07-20 fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
2012-07-20 blanchet 2012-07-20 renamed ML structures
2012-07-20 blanchet 2012-07-20 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
2012-07-18 blanchet 2012-07-18 speed up tautology/metaness check
2012-07-18 blanchet 2012-07-18 more consolidation of MaSh code
2012-07-18 blanchet 2012-07-18 drastic overhaul of MaSh data structures + fixed a few performance issues
2012-07-18 blanchet 2012-07-18 fixed order of accessibles + other tweaks to MaSh
2012-07-18 blanchet 2012-07-18 started implementing MaSh client-side I/O
2012-07-18 blanchet 2012-07-18 centrally construct expensive data structures
2012-07-11 blanchet 2012-07-11 moved most of MaSh exporter code to Sledgehammer
2012-07-11 blanchet 2012-07-11 further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
2012-07-10 blanchet 2012-07-10 MaSh evaluation driver
2012-07-10 blanchet 2012-07-10 moved MaSh into own files
2012-07-10 blanchet 2012-07-10 distinguish updates and queries + cleanups
2012-07-10 blanchet 2012-07-10 better tautology elimination
2012-07-10 blanchet 2012-07-10 generate lambdas and skolems again
2012-07-10 blanchet 2012-07-10 generate deep terms as feature
2012-07-10 blanchet 2012-07-10 generate theory name as a feature
2012-07-09 blanchet 2012-07-09 compile
2012-07-09 blanchet 2012-07-09 more precise dependencies -- eliminate tautologies
2012-07-09 blanchet 2012-07-09 generate problem file
2012-07-09 blanchet 2012-07-09 improve feature list generation