2005-07-13 avigad 2005-07-13 fixed typos in theorem names
2005-07-13 avigad 2005-07-13 Additions to the Real (and Hyperreal) libraries: RealDef.thy: lemmas relating nats, ints, and reals reversed direction of real_of_int_mult, etc. (now they agree with nat versions) SEQ.thy and Series.thy: various additions RComplete.thy: lemmas involving floor and ceiling introduced natfloor and natceiling Log.thy: various additions
2005-07-13 paulson 2005-07-13 tidied
2005-07-13 aspinall 2005-07-13 Add ISABELLE_PID for proof_general.ML
2005-07-13 wenzelm 2005-07-13 tuned msg;
2005-07-13 wenzelm 2005-07-13 added print_state_hook; renamed proof'' to actual_proof; tuned;
2005-07-13 wenzelm 2005-07-13 export previous;
2005-07-13 wenzelm 2005-07-13 removed ad-hoc atp_hook, cal_atp; removed depth_of; tuned;
2005-07-13 wenzelm 2005-07-13 Toplevel.actual_proof;
2005-07-13 wenzelm 2005-07-13 avoid excessive exceptions;
2005-07-13 wenzelm 2005-07-13 Graph: fast_string_ord;
2005-07-13 wenzelm 2005-07-13 export eq_brl;
2005-07-13 wenzelm 2005-07-13 added subtract; improved interface; tuned;
2005-07-13 wenzelm 2005-07-13 export eq_rrule; improved Net interface;
2005-07-13 wenzelm 2005-07-13 removed obsolete delta stuff;
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