2005-07-14 wenzelm 2005-07-14 tuned;
2005-07-14 wenzelm 2005-07-14 use all files in HOLCF.thy;
2005-07-14 wenzelm 2005-07-14 replaced Utils.itlist by fold_rev;
2005-07-14 wenzelm 2005-07-14 proper structure;
2005-07-14 wenzelm 2005-07-14 use existing Inttab;
2005-07-14 wenzelm 2005-07-14 improved oracle setup; replace itlist by fold_rev; replace end_itlist by Utils.end_itlist;
2005-07-14 wenzelm 2005-07-14 improved oracle setup;
2005-07-14 wenzelm 2005-07-14 removed not_const -- use Not instead; add mk_not;
2005-07-14 wenzelm 2005-07-14 HOL.Not; tuned;
2005-07-14 wenzelm 2005-07-14 HOL.Not;
2005-07-14 wenzelm 2005-07-14 new type-safe interface; added method example;
2005-07-14 wenzelm 2005-07-14 removed FOL/ex/IffOracle.ML;
2005-07-14 wenzelm 2005-07-14 obsolete;
2005-07-14 wenzelm 2005-07-14 improved 'oracle' command;
2005-07-14 wenzelm 2005-07-14 tuned;
2005-07-14 wenzelm 2005-07-14 accomodate change of real_of_XXX;
2005-07-14 obua 2005-07-14 - fixed bug concerning the renaming of axiom names - introduced new function Defs.fast_overloading_info
2005-07-14 haftmann 2005-07-14 added ` combinator
2005-07-14 haftmann 2005-07-14 (fix for smlnj)
2005-07-14 huffman 2005-07-14 simplified proof of cont_Iwhen3
2005-07-13 schirmer 2005-07-13 avoiding even more garbage
2005-07-13 aspinall 2005-07-13 Update PGIP packet handling, fixing unique session identifier.
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