2005-07-13 wenzelm 2005-07-13 open ReconPrelim Recon_Transfer;
2005-07-13 wenzelm 2005-07-13 open ReconPrelim ReconTranslateProof; removed second copy of exception ASSERTION;
2005-07-13 wenzelm 2005-07-13 tuned;
2005-07-13 wenzelm 2005-07-13 use Toplevel.print_state_hook instead of adhoc Proof.atp_hook; added call_atp: bool ref; do 'setmp print_mode []', which is more robust than manual ref manipulation; added subtract_simpset, subtract_claset (supercede delta approximation);
2005-07-13 wenzelm 2005-07-13 tuned concat_with_and; improved Net interface;
2005-07-13 wenzelm 2005-07-13 improved Net interface;
2005-07-13 wenzelm 2005-07-13 * Isar session: The initial use of ROOT.ML is now always timed;
2005-07-13 aspinall 2005-07-13 Add acceptedpgipelems message
2005-07-13 paulson 2005-07-13 auto update
2005-07-13 paulson 2005-07-13 generlization of some "nat" theorems
2005-07-13 paulson 2005-07-13 relevance filtering is now optional
2005-07-13 paulson 2005-07-13 tidied
2005-07-13 wenzelm 2005-07-13 fixed comment-out;
2005-07-13 obua 2005-07-13 fix
2005-07-13 aspinall 2005-07-13 Add management for current working directory
2005-07-13 haftmann 2005-07-13 (fix for an accidental commit)
2005-07-13 aspinall 2005-07-13 Note about theorem dependencies including themselves.
2005-07-13 aspinall 2005-07-13 Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
2005-07-13 haftmann 2005-07-13 (intermediate commit)
2005-07-13 haftmann 2005-07-13 (corrected wrong commit)
2005-07-13 haftmann 2005-07-13 (intermediate commit)
2005-07-13 obua 2005-07-13 - added cplex package to HOL/Matrix
2005-07-12 schirmer 2005-07-12 avoid some garbage
2005-07-12 obua 2005-07-12 - use TableFun instead of homebrew binary tree in am_interpreter.ML - add Floats to HOL/Real
2005-07-12 obua 2005-07-12 - introduce Pure/Tools directory - add compute oracle to Pure/Tools
2005-07-12 haftmann 2005-07-12 fold_map -> fold_yield, added transformator combinators, added selector combinator
2005-07-12 huffman 2005-07-12 changed orientation of bind_assoc rule
2005-07-12 huffman 2005-07-12 use qualified names for all constants
2005-07-12 huffman 2005-07-12 added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
2005-07-12 huffman 2005-07-12 generalized types of monadic operators to class cpo; added match function for UU
2005-07-12 avigad 2005-07-12 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.) renamed simplification rules for abs (abs_of_pos, etc.) renamed rules for multiplication and signs (mult_pos_pos, etc.) moved lemmas involving fractions from NatSimprocs.thy added setsum_mono3 to FiniteSet.thy added simplification rules for powers to Parity.thy
2005-07-12 paulson 2005-07-12 experimental code to reduce the amount of type information in blast
2005-07-12 paulson 2005-07-12 tweaked
2005-07-12 berghofe 2005-07-12 Added \<module> symbol.
2005-07-12 berghofe 2005-07-12 Added "attach" keyword for code generator setup.
2005-07-12 berghofe 2005-07-12 Auxiliary functions to be used in generated code are now defined using "attach".
2005-07-12 berghofe 2005-07-12 Implemented mechanism for attaching auxiliary code to consts_code and types_code declarations.
2005-07-11 nipkow 2005-07-11 small text mod
2005-07-11 quigley 2005-07-11 Fixed some problems with the signal handler.
2005-07-11 obua 2005-07-11 Improved implementation of Defs.is_overloaded.
2005-07-08 berghofe 2005-07-08 Some changes to allow mutually recursive, overloaded functions with same name.
2005-07-08 nipkow 2005-07-08 added Davenport reference
2005-07-08 nipkow 2005-07-08 moved Davenport citation to Main, removed author list
2005-07-08 nipkow 2005-07-08 moved gcd to new GCD.thy
2005-07-08 nipkow 2005-07-08 proof needed updating because of arith
2005-07-08 nipkow 2005-07-08 changed imports due to new GCD.thy
2005-07-08 nipkow 2005-07-08 Used to be in Library/Primes
2005-07-08 huffman 2005-07-08 fix typo
2005-07-08 huffman 2005-07-08 replaced old continuity rules with new lemma cont2cont_lift_case
2005-07-08 huffman 2005-07-08 simplified proof of ifte_thms, removed ifte_simp
2005-07-08 huffman 2005-07-08 renamed upE1 to upE; added simp rule cont2cont_flift1
2005-07-08 huffman 2005-07-08 renamed upE1 to upE
2005-07-08 huffman 2005-07-08 define 'a u with datatype package; removed obsolete lemmas; renamed upE1 to upE and Exh_Up1 to Exh_Up; cleaned up
2005-07-08 huffman 2005-07-08 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
2005-07-08 huffman 2005-07-08 add lemma eq_sprod
2005-07-08 huffman 2005-07-08 add lemma eq_cprod
2005-07-07 huffman 2005-07-07 removed obsolete continuity theorems
2005-07-07 huffman 2005-07-07 define lift type using pcpodef; cleaned up
2005-07-07 huffman 2005-07-07 cleaned up
2005-07-07 huffman 2005-07-07 fixes to work with UU_reorient_simproc