2012-03-28 bulwahn 2012-03-28 changing more definitions to quotient_definition
2012-03-28 bulwahn 2012-03-28 removing now redundant impl_of theorems in DAList
2012-03-28 bulwahn 2012-03-28 using abstract code equations for proofs of code equations in Multiset
2012-03-28 wenzelm 2012-03-28 simplified statements and proofs;
2012-03-28 wenzelm 2012-03-28 tuned whitespace;
2012-03-28 wenzelm 2012-03-28 updated Sign.add_type, Name_Space.declare;
2012-03-28 wenzelm 2012-03-28 updated comments;
2012-03-28 huffman 2012-03-28 merged
2012-03-27 huffman 2012-03-27 remove unnecessary rules from the simpset
2012-03-27 huffman 2012-03-27 remove unused premises
2012-03-27 huffman 2012-03-27 remove duplicate lemmas
2012-03-27 huffman 2012-03-27 mark some duplicate lemmas for deletion
2012-03-27 huffman 2012-03-27 remove more redundant lemmas
2012-03-27 huffman 2012-03-27 tuned proofs
2012-03-27 huffman 2012-03-27 remove redundant lemmas
2012-03-27 huffman 2012-03-27 generalized lemma zpower_zmod
2012-03-27 huffman 2012-03-27 remove redundant lemma
2012-03-27 huffman 2012-03-27 remove redundant lemma
2012-03-27 huffman 2012-03-27 remove duplicate [algebra] declarations
2012-03-27 huffman 2012-03-27 generalize more div/mod lemmas
2012-03-27 huffman 2012-03-27 generalize some theorems about div/mod
2012-03-28 wenzelm 2012-03-28 updated to jedit-4.5.1;
2012-03-27 kuncar 2012-03-27 merged
2012-03-27 kuncar 2012-03-27 note a code eqn in quotient_def
2012-03-27 boehmes 2012-03-27 dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
2012-03-27 blanchet 2012-03-27 more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)
2012-03-27 blanchet 2012-03-27 fixed eta-extension of higher-order quantifiers in THF output
2012-03-27 blanchet 2012-03-27 renamed "smt_fixed" to "smt_read_only_certificates"
2012-03-27 blanchet 2012-03-27 tuning
2012-03-27 blanchet 2012-03-27 tuning (in particular, Symtab instead of AList)
2012-03-27 blanchet 2012-03-27 tweak slices, based on eval by Daniel Wand
2012-03-27 blanchet 2012-03-27 be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
2012-03-27 blanchet 2012-03-27 print a hint
2012-03-27 blanchet 2012-03-27 avoid DL
2012-03-27 blanchet 2012-03-27 TFF: declare free types as types
2012-03-27 bulwahn 2012-03-27 merged
2012-03-27 bulwahn 2012-03-27 association lists with distinct keys uses the quotient infrastructure to obtain code certificates; added remarks about further improvements
2012-03-27 huffman 2012-03-27 remove redundant lemmas
2012-03-27 huffman 2012-03-27 move int::ring_div instance upward, simplify several proofs
2012-03-27 huffman 2012-03-27 rename lemmas {divmod_int_rel_{div,mod} -> {div,mod}_int_unique, for consistency with nat lemma names
2012-03-27 huffman 2012-03-27 extend definition of divmod_int_rel to handle denominator=0 case
2012-03-27 huffman 2012-03-27 tuned proofs
2012-03-27 huffman 2012-03-27 shorten a proof
2012-03-27 huffman 2012-03-27 simplify some proofs
2012-03-27 huffman 2012-03-27 rename lemmas {div,mod}_eq -> {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
2012-03-27 huffman 2012-03-27 simplify some proofs
2012-03-26 wenzelm 2012-03-26 merged
2012-03-26 nipkow 2012-03-26 merged
2012-03-26 nipkow 2012-03-26 reverted to canonical name
2012-03-26 wenzelm 2012-03-26 merged
2012-03-26 huffman 2012-03-26 merged
2012-03-26 huffman 2012-03-26 revert changeset 500a5d97511a, re-enabling HOL-Proofs-Lambda
2012-03-26 huffman 2012-03-26 merged
2012-03-26 huffman 2012-03-26 fix incorrect code_modulename declarations
2012-03-26 huffman 2012-03-26 code lemma for function 'nat' that doesn't go into an infinite loop (fixes problem with non-terminating HOL-Proofs-Lambda)
2012-03-26 huffman 2012-03-26 remove old-style semicolon
2012-03-26 nipkow 2012-03-26 merged
2012-03-26 nipkow 2012-03-26 Functions and lemmas by Christian Sternagel
2012-03-26 wenzelm 2012-03-26 more precise treatment of \r\n as blank symbol (cf. 2bf29095d26f), e.g. relevant for loading theory headers in Isabelle/jEdit -- NB: jEdit and Isabelle/ML normalize newline variants to \n, but Isabelle/Scala retains them literally;
2012-03-26 wenzelm 2012-03-26 disabled HOL-Proofs-Lambda temporarily, which causes problems with 2a1953f0d20d;