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
2012-04-20 huffman 2012-04-20 rename 'correspondence' method to 'transfer_prover'
2012-04-20 kuncar 2012-04-20 hide the invariant constant for relators: invariant_commute infrastracture
2012-04-20 wenzelm 2012-04-20 improved interleaving of start_execution vs. cancel_execution of the next update;
2012-04-20 wenzelm 2012-04-20 tuned proofs;
2012-04-20 wenzelm 2012-04-20 always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;
2012-04-20 wenzelm 2012-04-20 tuned;
2012-04-20 wenzelm 2012-04-20 simplified internal actor protocol;
2012-04-20 wenzelm 2012-04-20 builtin timing for main operations;
2012-04-20 huffman 2012-04-20 add secondary transfer rule for universal quantifiers on non-bi-total relations
2012-04-20 huffman 2012-04-20 move definition of set_rel into Library/Quotient_Set.thy
2012-04-20 huffman 2012-04-20 add transfer rule for 'id'
2012-04-20 huffman 2012-04-20 add new transfer rules and setup for lifting package
2012-04-20 huffman 2012-04-20 setup_lifting preprocesses forall_transfer rule by unfolding mem_Collect_eq
2012-04-20 hoelzl 2012-04-20 NEWS
2012-04-20 hoelzl 2012-04-20 hide code generation facts in the Float theory, they are only exported for Approximation
2012-04-20 nipkow 2012-04-20 merged
2012-04-20 nipkow 2012-04-20 forgot to add file
2012-04-20 huffman 2012-04-20 make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
2012-04-19 wenzelm 2012-04-19 merged
2012-04-19 hoelzl 2012-04-19 NEWS
2012-04-19 hoelzl 2012-04-19 transfer now handles Let
2012-04-19 nipkow 2012-04-19 merged
2012-04-19 nipkow 2012-04-19 added revised version of Abs_Int