2012-04-23 hoelzl 2012-04-23 CONTRIBUTORS
2012-04-23 hoelzl 2012-04-23 reworked Probability theory
2012-04-23 sultana 2012-04-23 updated test;
2012-04-23 sultana 2012-04-23 improved non-interpretation of constants and numbers; improved interpretation of terms and formulas; tuned;
2012-04-23 sultana 2012-04-23 improved interpreting conditionals; tuned;
2012-04-23 sultana 2012-04-23 disabled interpreting arithmetic;
2012-04-23 sultana 2012-04-23 improved handling of single-quoted names;
2012-04-23 sultana 2012-04-23 disabled exception packaging in tptp;
2012-04-23 sultana 2012-04-23 moved function for testing problem-name parsing; list of TPTP test files not immediately evaluated;
2012-04-23 sultana 2012-04-23 removed redundant function;
2012-04-22 wenzelm 2012-04-22 bundle Isabelle.exe;
2012-04-22 huffman 2012-04-22 tuned precedence order of transfer rules
2012-04-22 wenzelm 2012-04-22 updated generated files;
2012-04-22 wenzelm 2012-04-22 updated const "relcomp";
2012-04-22 wenzelm 2012-04-22 merged
2012-04-22 huffman 2012-04-22 add transfer rule for set difference
2012-04-22 wenzelm 2012-04-22 support Cygwin cold-start via Isabelle.exe, assuming layout of bundle;
2012-04-22 wenzelm 2012-04-22 merged
2012-04-22 huffman 2012-04-22 merged
2012-04-22 huffman 2012-04-22 adapt to changes in generated transfer rules (cf. 4483c004499a)
2012-04-22 huffman 2012-04-22 fix bug caused by misunderstanding of operator precedences (cf. cb44d09d9d22)
2012-04-22 wenzelm 2012-04-22 more robust handling of PATH vs PATH_JVM -- required for cold start of Cygwin from Windows (e.g. Isabelle.exe);
2012-04-22 wenzelm 2012-04-22 merged
2012-04-22 blanchet 2012-04-22 fixed typos
2012-04-22 blanchet 2012-04-22 tried harder to make SML/NJ happy
2012-04-22 blanchet 2012-04-22 added timeout argument to TPTP tools
2012-04-22 blanchet 2012-04-22 fix bug where "==" was used instead of "HOL.eq"
2012-04-22 blanchet 2012-04-22 more meaningful default value
2012-04-22 blanchet 2012-04-22 handle exception (needed to solve TPTP problem SEU880^5)
2012-04-22 wenzelm 2012-04-22 pretend jedit is up-to-date if this is not a repository -- avoid accidental build attempts after touching files etc.;
2012-04-22 wenzelm 2012-04-22 refer to isabelle.Main application wrapper;
2012-04-22 wenzelm 2012-04-22 display return code like Isabelle.app on Mac OS;
2012-04-22 wenzelm 2012-04-22 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
2012-04-22 wenzelm 2012-04-22 updated Isabelle.exe specification, assuming layout of bundle;
2012-04-22 wenzelm 2012-04-22 USER_HOME settings variable points to cross-platform user home directory;
2012-04-22 huffman 2012-04-22 new example theory for quotient/transfer
2012-04-21 huffman 2012-04-21 update NEWS for transfer/quotient
2012-04-21 huffman 2012-04-21 enable variant of transfer method that proves an implication instead of an equivalence
2012-04-19 haftmann 2012-04-19 moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
2012-04-21 wenzelm 2012-04-21 merged
2012-04-21 huffman 2012-04-21 NEWS for transfer, lifting, and quotient
2012-04-21 huffman 2012-04-21 new example theory for transfer package
2012-04-21 wenzelm 2012-04-21 some builtin session timing;
2012-04-21 huffman 2012-04-21 move alternative definition lemmas into Lifting.thy; simplify proof of Quotient_compose
2012-04-21 huffman 2012-04-21 tuned proofs
2012-04-21 huffman 2012-04-21 add transfer rule for List.set
2012-04-21 huffman 2012-04-21 remove duplicate of lemma id_transfer
2012-04-21 huffman 2012-04-21 added covariant relator set_rel, with transfer rules for set operations
2012-04-21 huffman 2012-04-21 renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
2012-04-21 blanchet 2012-04-21 tried to make SML/NJ happy
2012-04-21 blanchet 2012-04-21 tuned "max_relevant" defaults for SMT solvers based on Judgment Day
2012-04-21 blanchet 2012-04-21 prepend PWD to relative paths
2012-04-21 blanchet 2012-04-21 reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
2012-04-21 blanchet 2012-04-21 swap out Satallax, pull in E-SInE again -- it's not clear yet how useful Satallax is after proof reconstruction, whereas E-SInE performed surprisingly well on latest evaluations
2012-04-21 huffman 2012-04-21 new transfer package rules and lifting setup for lists
2012-04-21 huffman 2012-04-21 strengthen rule list_all2_induct
2012-04-20 wenzelm 2012-04-20 more standard Theory_Data setup; keep meta-comments within the history;
2012-04-20 wenzelm 2012-04-20 merged
2012-04-20 huffman 2012-04-20 add transfer rule for nat_case
2012-04-20 huffman 2012-04-20 uniform naming scheme for transfer rules