Mercurialisabelle / shortlog
summary | shortlog | changelog | graph | tags | branches | files | gz

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