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
2012-04-19 huffman 2012-04-19 add transfer rule for Let
2012-04-19 huffman 2012-04-19 add code lemmas for word operations
2012-04-19 haftmann 2012-04-19 tuned whitespace
2012-04-19 haftmann 2012-04-19 dropped dead code
2012-04-19 kuncar 2012-04-19 rename no_code to no_abs_code - more appropriate name
2012-04-19 kuncar 2012-04-19 use tnames for bound variables in rsp thms
2012-04-19 blanchet 2012-04-19 true delayed evaluation of "SPASS_VERSION" environment variable
2012-04-19 blanchet 2012-04-19 merged
2012-04-19 blanchet 2012-04-19 use latest Z3
2012-04-19 nipkow 2012-04-19 merged