2011-06-09 wenzelm 2011-06-09 merged
2011-06-09 bulwahn 2011-06-09 merged
2011-06-09 bulwahn 2011-06-09 resolving an issue with class instances that are pseudo functions in the OCaml code serializer
2011-06-09 hoelzl 2011-06-09 merged
2011-06-09 hoelzl 2011-06-09 fixed document generation for HOL
2011-06-09 hoelzl 2011-06-09 lemma: independence is equal to mutual information = 0
2011-06-09 hoelzl 2011-06-09 jensens inequality
2011-06-09 hoelzl 2011-06-09 lemmas about right derivative and limits
2011-06-09 hoelzl 2011-06-09 lemma about differences of convex functions
2011-06-09 hoelzl 2011-06-09 lemmas relating ln x and x - 1
2011-05-31 hoelzl 2011-05-31 use divide instead of inverse for the derivative of ln
2011-06-09 bulwahn 2011-06-09 adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10
2011-06-09 wenzelm 2011-06-09 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-06-09 wenzelm 2011-06-09 document depth arguments of method "auto";
2011-06-09 wenzelm 2011-06-09 clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b); uniform handling of exceptions in depth_tac and blast_tac, discontinued separate blast_depth_tac; tuned blast_tac: atomize prems only once, outside DEEPEN;
2011-06-09 wenzelm 2011-06-09 clarified special incr_type_indexes;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-06-08 wenzelm 2011-06-08 modernized structure ProofContext;
2011-06-09 wenzelm 2011-06-09 even more robust \isaspacing;
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-06-09 wenzelm 2011-06-09 some attempts at robust \isaspacing so that \isa{...} can be used in section headings etc. (need to avoid `\? for some reason);
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-06-09 wenzelm 2011-06-09 prefer new-style Name.invents;
2011-06-09 wenzelm 2011-06-09 more tight name invention -- avoiding old functions;
2011-06-09 wenzelm 2011-06-09 \frenchspacing for formal isabelle style avoids extra space in situations like ``@{text "?"}'' followed by plain text;
2011-06-09 wenzelm 2011-06-09 tuned;
2011-06-09 bulwahn 2011-06-09 NEWS
2011-06-09 bulwahn 2011-06-09 correcting import theory of examples
2011-06-09 bulwahn 2011-06-09 fixing code generation test
2011-06-09 bulwahn 2011-06-09 removing char setup
2011-06-09 bulwahn 2011-06-09 removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
2011-06-09 bulwahn 2011-06-09 adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
2011-06-09 bulwahn 2011-06-09 adding narrowing engine for existentials
2011-06-09 bulwahn 2011-06-09 adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
2011-06-09 bulwahn 2011-06-09 adding theory Quickcheck_Narrowing to HOL-Main image
2011-06-09 bulwahn 2011-06-09 adapting IsaMakefile
2011-06-09 bulwahn 2011-06-09 moving Quickcheck_Narrowing from Library to base directory
2011-06-09 bulwahn 2011-06-09 compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
2011-06-09 bulwahn 2011-06-09 local simp rule in List_Cset
2011-06-09 blanchet 2011-06-09 tuning
2011-06-09 blanchet 2011-06-09 compile
2011-06-09 blanchet 2011-06-09 cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
2011-06-09 blanchet 2011-06-09 added a really fully typed translation as a fallback for Metis, in rare cases where Metis correctly proves a theorem but has type-unsound steps in it (which is likelier to happen with some of the lighter translations)
2011-06-09 blanchet 2011-06-09 improve sort inference in Metis proofs -- in some rare cases Metis steals Isabelle's variable names and the sorts must then be inferred as well
2011-06-09 blanchet 2011-06-09 removed needless function that duplicated standard functionality, with a little unnecessary twist
2011-06-09 blanchet 2011-06-09 removed more dead code
2011-06-09 blanchet 2011-06-09 be a bit more liberal with respect to the universal sort -- it sometimes help
2011-06-09 blanchet 2011-06-09 renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
2011-06-08 wenzelm 2011-06-08 merged
2011-06-08 blanchet 2011-06-08 avoid duplicate facts, which confuse the minimizer output
2011-06-08 blanchet 2011-06-08 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
2011-06-08 blanchet 2011-06-08 restore comment about subtle issue
2011-06-08 blanchet 2011-06-08 made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded
2011-06-08 blanchet 2011-06-08 don't launch the automatic minimizer for zero facts
2011-06-08 blanchet 2011-06-08 don't generate unsound proof error for missing proofs
2011-06-08 blanchet 2011-06-08 renamed option to avoid talking about seconds, since this is now the default Isabelle unit
2011-06-08 blanchet 2011-06-08 fixed format selection logic for Waldmeister
2011-06-08 blanchet 2011-06-08 better default type system for Waldmeister, with fewer predicates (for types or type classes)
2011-06-08 wenzelm 2011-06-08 simplified directory structure; recovered README.html;
2011-06-08 wenzelm 2011-06-08 simplified directory structure;