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
2011-09-07 blanchet 2011-09-07 parse new experimental '@' encodings
2011-09-07 blanchet 2011-09-07 tuning
2011-09-07 blanchet 2011-09-07 tuning
2011-09-07 blanchet 2011-09-07 tuning
2011-09-07 wenzelm 2011-09-07 clarified import;
2011-09-07 wenzelm 2011-09-07 tuned/simplified proofs;
2011-09-07 wenzelm 2011-09-07 tuned proofs;
2011-09-07 wenzelm 2011-09-07 deactivate unfinished charset provider for now, to avoid user confusion;
2011-09-07 wenzelm 2011-09-07 more NEWS;
2011-09-07 wenzelm 2011-09-07 added "check" button: adhoc change to full buffer perspective;
2011-09-07 wenzelm 2011-09-07 added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
2011-09-07 blanchet 2011-09-07 separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
2011-09-07 blanchet 2011-09-07 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
2011-09-07 blanchet 2011-09-07 tuning
2011-09-07 blanchet 2011-09-07 make mangling sound w.r.t. type arguments
2011-09-07 blanchet 2011-09-07 make "filter_type_args" more robust if the actual arity is higher than the declared one
2011-09-07 blanchet 2011-09-07 updated Sledgehammer documentation
2011-09-07 blanchet 2011-09-07 rationalize uniform encodings
2011-09-06 huffman 2011-09-06 merged
2011-09-06 huffman 2011-09-06 avoid using legacy theorem names
2011-09-06 huffman 2011-09-06 merged
2011-09-06 huffman 2011-09-06 remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
2011-09-07 Cezary Kaliszyk 2011-09-07 HOL/Import: Update HOL4 generated files to current Isabelle.
2011-09-07 wenzelm 2011-09-07 tuned proofs;