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;
2012-03-26 kuncar 2012-03-26 tuned comment
2012-03-26 kuncar 2012-03-26 merged
2012-03-26 kuncar 2012-03-26 merged
2012-03-26 kuncar 2012-03-26 tuned proof - no smt call
2012-03-26 wenzelm 2012-03-26 more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
2012-03-26 wenzelm 2012-03-26 updated theory header syntax and related details;
2012-03-24 wenzelm 2012-03-24 ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE); update for prospective jdk1.7.x component;
2012-03-26 wenzelm 2012-03-26 merged
2012-03-26 blanchet 2012-03-26 reintroduced broken proofs and regenerated certificates
2012-03-26 wenzelm 2012-03-26 merged, resolving trivial conflict;
2012-03-26 blanchet 2012-03-26 fixed Nitpick after numeral representation change (2a1953f0d20d)
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-24 kuncar 2012-03-24 merged
2012-03-23 kuncar 2012-03-23 use Thm.transfer for thms stored in generic context data storage
2012-03-23 kuncar 2012-03-23 hide invariant constant
2012-03-24 wenzelm 2012-03-24 explicit SMTP server (appears to be required after recent change of system configuration);
2012-03-24 wenzelm 2012-03-24 more isatest subscribers;
2012-03-23 paulson 2012-03-23 merged
2012-03-23 paulson 2012-03-23 proof tidying