2012-04-28 wenzelm 2012-04-28 some coverage of Isabelle/Scala tools;
2012-04-28 wenzelm 2012-04-28 some coverage of Isabelle/jEdit;
2012-04-28 wenzelm 2012-04-28 some manual updates;
2012-04-28 wenzelm 2012-04-28 some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x; removed historic note about Poly/ML vs. SML/NJ;
2012-04-28 huffman 2012-04-28 add isar-ref documentation for transfer package
2012-04-28 haftmann 2012-04-28 less confusion in NEWS
2012-04-28 haftmann 2012-04-28 rhs of abstract code equations are not subject to preprocessing: inline code abbrevs explicitly
2012-04-28 nipkow 2012-04-28 renamed Semi to Seq
2012-04-27 wenzelm 2012-04-27 merged
2012-04-27 wenzelm 2012-04-27 prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;
2012-04-27 wenzelm 2012-04-27 clarified signature;
2012-04-27 wenzelm 2012-04-27 avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich;
2012-04-27 wenzelm 2012-04-27 made Context_Position independent from Config;
2012-04-27 blanchet 2012-04-27 use Nitpick as an oracle for finite problems
2012-04-27 blanchet 2012-04-27 add extensionality to first-order provers
2012-04-27 blanchet 2012-04-27 avoid duplicate helpers
2012-04-27 wenzelm 2012-04-27 mention tools and packages earlier;
2012-04-27 wenzelm 2012-04-27 tuned;
2012-04-27 wenzelm 2012-04-27 tuned;
2012-04-27 wenzelm 2012-04-27 tuned;
2012-04-27 wenzelm 2012-04-27 tuned;
2012-04-27 wenzelm 2012-04-27 merged
2012-04-27 huffman 2012-04-27 allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing
2012-04-27 kuncar 2012-04-27 documentation for the Lifting package in Isar-ref
2012-04-27 wenzelm 2012-04-27 added darwin targets;
2012-04-27 wenzelm 2012-04-27 chmod -x;
2012-04-27 wenzelm 2012-04-27 multi-platform build script and component settings;
2012-04-27 wenzelm 2012-04-27 print errors on stderr;
2012-04-27 wenzelm 2012-04-27 general exec_process -- nothing specific to Cygwin;
2012-04-27 wenzelm 2012-04-27 more direct exec with synchronous exit code;
2012-04-27 wenzelm 2012-04-27 some updates on classic README, reduce the impression that there is much to install manually;
2012-04-27 blanchet 2012-04-27 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
2012-04-27 blanchet 2012-04-27 move LEO-II closer to the top, for testing
2012-04-27 blanchet 2012-04-27 get rid of old CASC setup and move the arithmetic part to a new theory
2012-04-27 blanchet 2012-04-27 smaller batches, to play safe
2012-04-27 blanchet 2012-04-27 move file to where it belongs
2012-04-27 huffman 2012-04-27 implement transfer tactic with more scalable forward proof methods
2012-04-27 blanchet 2012-04-27 tuning
2012-04-27 blanchet 2012-04-27 tweak LEO-II setup
2012-04-27 blanchet 2012-04-27 eta-expand unapplied equalities in THF rather than using a proxy
2012-04-27 blanchet 2012-04-27 more tweaking of TPTP/CASC setup
2012-04-26 kuncar 2012-04-26 added a basic sanity check for quot_map
2012-04-26 wenzelm 2012-04-26 tuned comment;
2012-04-26 blanchet 2012-04-26 fixed bug in handling of new numerals -- the left-hand side of "Numeral1 = 1" should be left alone and not translated to a built-in Kodkod numeral in the specification of the "numeral" function
2012-04-26 wenzelm 2012-04-26 merged
2012-04-26 hoelzl 2012-04-26 add code equation for real_of_float
2012-04-26 kuncar 2012-04-26 tuned; don't generate abs code if quotient_type is used
2012-04-26 kuncar 2012-04-26 support Quotient map theorems with invariant parameters
2012-04-26 kuncar 2012-04-26 use a quot_map theorem attribute instead of the complicated map attribute
2012-04-26 blanchet 2012-04-26 further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
2012-04-26 blanchet 2012-04-26 put Satallax first, at least for now (useful for experiments)
2012-04-26 blanchet 2012-04-26 tuning
2012-04-26 blanchet 2012-04-26 tuning
2012-04-26 blanchet 2012-04-26 tentatively tag hypotheses as definition -- this sometimes help the "tptp_sledgehammer" tool (e.g. SEU466^1.p)
2012-04-26 blanchet 2012-04-26 tuning; no need for relevance filter
2012-04-25 blanchet 2012-04-25 tuning
2012-04-25 blanchet 2012-04-25 don't extensionalize formulas for higher-order provers -- Satallax in particular will only expand definitions of the form "constant = ..."
2012-04-25 blanchet 2012-04-25 don't use the native choice operator if the type encoding isn't higher-order
2012-04-25 blanchet 2012-04-25 tuning
2012-04-25 blanchet 2012-04-25 more work on TPTP Isabelle and Sledgehammer tactics