remove redundant lemma complex_of_real_minus_one

simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma

removed unused lemma sin_cos_squared_add2_mult

remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq

avoid using legacy theorem names

merged

theory of saturated naturals contributed by Peter Gammie

theory of saturated naturals contributed by Peter Gammie

lemmas about +, *, min, max on nat

update Sledgehammer docs

added new tagged encodings to Metis tests

also implemented ghost version of the tagged encodings

added new guards encoding to test

smarter explicit apply business

started work on ghost type arg encoding

stricted type encoding parsing

more substructural sharing to gain significant compression;

XML.cache for partial sharing (strings only);

platform-specific look and feel;

more README;

clarified terminology;

no print_state for final proof commands, which return to theory state;

NEWS on IsabelleText font;

explicit join_syntax ensures command transaction integrity of 'theory';

some updates for release;

some tuning for release;

updated file locations;

merged

merged

removing previously used function locally_monomorphic in the code generator

setting const_sorts to false in the type inference of the code generator

adapting Imperative HOL serializer to changes of the iterm datatype in the code generator

removing previous crude approximation to add type annotations to disambiguate types

adding minimalistic implementation for printing the type annotations

adding call to disambiguation annotations

adding type inference for disambiguation annotations in code equation

adding the body type as well to the code generation for constants as it is required for type annotations of constants

changing const type to pass along if typing annotations are necessary for disambigous terms

fixed THF type constructor syntax

tweaking polymorphic TFF and THF output

parse new experimental '@' encodings

tuning

tuning

tuning

clarified import;

tuned/simplified proofs;

tuned proofs;

deactivate unfinished charset provider for now, to avoid user confusion;

more NEWS;

added "check" button: adhoc change to full buffer perspective;

added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);

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

perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s

tuning

make mangling sound w.r.t. type arguments

make "filter_type_args" more robust if the actual arity is higher than the declared one

updated Sledgehammer documentation

rationalize uniform encodings

merged

avoid using legacy theorem names