2010-09-02 haftmann 2010-09-02 formal markup of generated code for statements
2010-09-02 haftmann 2010-09-02 removed namespace stuff from code_printer
2010-09-02 blanchet 2010-09-02 merged
2010-09-02 blanchet 2010-09-02 reenable Nitpick on Cygwin; we'll see tomorrow if there's still a failure, and if so I'll investigate
2010-09-03 wenzelm 2010-09-03 merged;
2010-09-03 wenzelm 2010-09-03 Proof.pretty_state: print everything in the foreground context to give users a chance to configure options, e.g. via "using [[show_consts]]";
2010-09-03 wenzelm 2010-09-03 turned show_consts into proper configuration option;
2010-09-03 wenzelm 2010-09-03 prefer regular Proof.context over background theory; misc tuning and simplification;
2010-09-02 wenzelm 2010-09-02 just one refute.ML;
2010-09-02 wenzelm 2010-09-02 use existing Integer.pow, despite its slightly odd argument order;
2010-09-02 wenzelm 2010-09-02 tuned whitespace and indentation, emphasizing the logical structure of this long text;
2010-09-02 wenzelm 2010-09-02 inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;
2010-09-02 wenzelm 2010-09-02 Document_View: squiggly underline for messages; tuned;
2010-09-02 wenzelm 2010-09-02 added gfx_range convenience;
2010-09-02 wenzelm 2010-09-02 Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
2010-09-02 wenzelm 2010-09-02 Position.Range: exclude singularity (again);
2010-09-02 wenzelm 2010-09-02 merged
2010-09-02 blanchet 2010-09-02 merged
2010-09-02 blanchet 2010-09-02 FIXME -> TODO (nothing is broken)
2010-09-02 blanchet 2010-09-02 Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
2010-09-02 blanchet 2010-09-02 use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this *really* speeds up things -- HOL now builds 12% faster on my machine
2010-09-02 blanchet 2010-09-02 make definitional CNF translation code more robust in the presence of existential quantifiers in the "literals"
2010-09-02 haftmann 2010-09-02 formal framework for presentation of selected statements
2010-09-02 haftmann 2010-09-02 merged
2010-09-02 haftmann 2010-09-02 Table.map replaces Table.map'
2010-09-02 haftmann 2010-09-02 dropped dead code; tuned
2010-09-02 haftmann 2010-09-02 include names need not be considered as reserved any longer
2010-09-02 haftmann 2010-09-02 skip empty name bunches; fill up trailing positions with NONEs
2010-09-02 haftmann 2010-09-02 use code_namespace module for SML and OCaml code
2010-09-02 haftmann 2010-09-02 Table.map replaces Table.map'
2010-09-02 haftmann 2010-09-02 avoid cyclic modules
2010-09-02 haftmann 2010-09-02 merged
2010-09-01 haftmann 2010-09-01 simultaneous modification of statements: statement names
2010-09-01 haftmann 2010-09-01 simultaneous modification of statements
2010-09-01 haftmann 2010-09-01 explicit modify_stmt parameter
2010-09-01 haftmann 2010-09-01 Graph.map, in analogy to Table.map
2010-09-01 haftmann 2010-09-01 replaced Table.map' by Table.map
2010-09-01 haftmann 2010-09-01 merged
2010-09-01 haftmann 2010-09-01 tuned
2010-09-01 haftmann 2010-09-01 generalized hierarchical data structure over statements
2010-09-02 haftmann 2010-09-02 merged
2010-09-02 haftmann 2010-09-02 normalization is allowed to solve True
2010-09-02 blanchet 2010-09-02 merged
2010-09-02 blanchet 2010-09-02 merged
2010-09-02 blanchet 2010-09-02 cosmetics
2010-09-02 blanchet 2010-09-02 SNARK doesn't like facts
2010-09-02 blanchet 2010-09-02 show real CPU time
2010-09-01 blanchet 2010-09-01 factor out code shared by all ATPs so that it's run only once
2010-09-01 blanchet 2010-09-01 handle all whitespace, not just ASCII 32
2010-09-01 blanchet 2010-09-01 speed up SPASS hack + output time information in "blocking" mode
2010-09-01 blanchet 2010-09-01 remove time information in output, since it's confusing anyway
2010-09-01 blanchet 2010-09-01 minor refactoring
2010-09-01 blanchet 2010-09-01 translate the axioms to FOF once and for all ATPs
2010-09-01 blanchet 2010-09-01 run relevance filter in a thread, to avoid blocking
2010-09-01 blanchet 2010-09-01 add dependency of "spass" script
2010-09-01 blanchet 2010-09-01 more elegant ML
2010-09-01 blanchet 2010-09-01 only kill ATP threads in nonblocking mode
2010-09-01 blanchet 2010-09-01 lower number of facts given to SInE
2010-09-01 blanchet 2010-09-01 share the relevance filter among the provers
2010-09-01 blanchet 2010-09-01 got rid of the "theory_relevant" option; instead, have fudge factors that behave more smoothly for all provers