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