2011-09-09 krauss 2011-09-09 added syntactic classes for "inf" and "sup"
2011-09-08 huffman 2011-09-08 prove existence, uniqueness, and other properties of complex arg function
2011-09-08 huffman 2011-09-08 tuned
2011-09-08 huffman 2011-09-08 remove obsolete intermediate lemma complex_inverse_complex_split
2011-09-08 huffman 2011-09-08 tuned
2011-09-08 haftmann 2011-09-08 merged
2011-09-08 haftmann 2011-09-08 tuned
2011-09-08 haftmann 2011-09-08 merged
2011-09-07 haftmann 2011-09-07 merged
2011-09-06 haftmann 2011-09-06 merged
2011-09-06 haftmann 2011-09-06 merged
2011-09-06 haftmann 2011-09-06 merged
2011-09-05 haftmann 2011-09-05 tuned
2011-09-05 haftmann 2011-09-05 merged
2011-09-05 haftmann 2011-09-05 tuned
2011-09-04 haftmann 2011-09-04 tuned
2011-09-08 blanchet 2011-09-08 fixed computation of "in_conj" for polymorphic encodings
2011-09-07 huffman 2011-09-07 add some new lemmas about cis and rcis; simplify some proofs;
2011-09-07 huffman 2011-09-07 Complex.thy: move theorems into appropriate subsections
2011-09-07 huffman 2011-09-07 merged
2011-09-07 huffman 2011-09-07 remove redundant lemma complex_of_real_minus_one
2011-09-07 huffman 2011-09-07 simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
2011-09-07 huffman 2011-09-07 removed unused lemma sin_cos_squared_add2_mult
2011-09-07 huffman 2011-09-07 remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
2011-09-07 huffman 2011-09-07 avoid using legacy theorem names
2011-09-08 wenzelm 2011-09-08 merged
2011-09-07 haftmann 2011-09-07 theory of saturated naturals contributed by Peter Gammie
2011-09-07 haftmann 2011-09-07 theory of saturated naturals contributed by Peter Gammie
2011-09-07 haftmann 2011-09-07 lemmas about +, *, min, max on nat
2011-09-07 blanchet 2011-09-07 update Sledgehammer docs
2011-09-07 blanchet 2011-09-07 added new tagged encodings to Metis tests
2011-09-07 blanchet 2011-09-07 also implemented ghost version of the tagged encodings
2011-09-07 blanchet 2011-09-07 added new guards encoding to test
2011-09-07 blanchet 2011-09-07 smarter explicit apply business
2011-09-07 blanchet 2011-09-07 started work on ghost type arg encoding
2011-09-07 blanchet 2011-09-07 stricted type encoding parsing
2011-09-08 wenzelm 2011-09-08 more substructural sharing to gain significant compression;
2011-09-07 wenzelm 2011-09-07 XML.cache for partial sharing (strings only);
2011-09-07 wenzelm 2011-09-07 platform-specific look and feel;
2011-09-07 wenzelm 2011-09-07 more README;
2011-09-07 wenzelm 2011-09-07 clarified terminology;
2011-09-07 wenzelm 2011-09-07 no print_state for final proof commands, which return to theory state;
2011-09-07 wenzelm 2011-09-07 NEWS on IsabelleText font;
2011-09-07 wenzelm 2011-09-07 explicit join_syntax ensures command transaction integrity of 'theory';
2011-09-07 wenzelm 2011-09-07 some updates for release;
2011-09-07 wenzelm 2011-09-07 some tuning for release;
2011-09-07 wenzelm 2011-09-07 updated file locations;
2011-09-07 wenzelm 2011-09-07 merged
2011-09-07 bulwahn 2011-09-07 merged
2011-09-07 bulwahn 2011-09-07 removing previously used function locally_monomorphic in the code generator
2011-09-07 bulwahn 2011-09-07 setting const_sorts to false in the type inference of the code generator
2011-09-07 bulwahn 2011-09-07 adapting Imperative HOL serializer to changes of the iterm datatype in the code generator
2011-09-07 bulwahn 2011-09-07 removing previous crude approximation to add type annotations to disambiguate types
2011-09-07 bulwahn 2011-09-07 adding minimalistic implementation for printing the type annotations
2011-09-07 bulwahn 2011-09-07 adding call to disambiguation annotations
2011-09-07 bulwahn 2011-09-07 adding type inference for disambiguation annotations in code equation
2011-09-07 bulwahn 2011-09-07 adding the body type as well to the code generation for constants as it is required for type annotations of constants
2011-09-07 bulwahn 2011-09-07 changing const type to pass along if typing annotations are necessary for disambigous terms
2011-09-07 blanchet 2011-09-07 fixed THF type constructor syntax
2011-09-07 blanchet 2011-09-07 tweaking polymorphic TFF and THF output