NEWS and CONTRIBUTORS

remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def

simplify proofs using LIMSEQ lemmas

remove trivial lemma Lim_at_iff_LIM

fix typos

NEWS for euclidean_space class

move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy

adding NEWS and CONTRIBUTORS

merged

correcting imports after splitting and renaming AssocList

tuned

moving connection of association lists to Mappings into a separate theory

adding NEWS and CONTRIBUTORS

tuned some symbol that probably went there by some strange encoding issue

added my contributions to NEWS and CONTRIBUTORS

fixed type intersection (again)

consistent option naming

NEWS fastsimp -> fastforce

new fastforce replacing fastsimp - less confusing name

merged

NEWS for Library/Product_Lattice.thy

misc tuning and clarification;

merged

merged

tuned proofs

Library/Saturated.thy: 'Sat' abbreviates 'of_nat'

more CONTRIBUTORS;

persistent ISABELLE_INTERFACE_CHOICE;

explicit choice of interface;

more orthogonal signature;

updates for release;

misc tuning and clarification (NB: settings are already local for named snapshots/releases);

some updates of PLATFORMS;

more README;

merged

mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)

misc tuning;

misc tuning and clarification;

speed up slow proof;

merged

more modularization

stronger colors (as background);

some color scheme for theory status;

some keyboard shortcuts for important actions; proper label properties, which are also required for jEdit "Shortcuts" options panel;

explicit jEdit actions -- to enable key mappings, for example;

more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;

tuned usage;

simplified default Isabelle application wrapper (NB: build process is already part of isabelle jedit tool);

renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.

fixed definition of type intersection (soundness bug)

continue with minimization in debug mode in spite of unsoundness

generalize lemma of_nat_number_of_eq to class number_semiring

merged

stating more explicitly our expectation that these two terms have the same term structure

revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types

made SML/NJ happy

call ghc with -XEmptyDataDecls

merged

tuned headers

Library/Saturated.thy: number_semiring class instance

remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}

merged

remove unnecessary intermediate lemmas

added syntactic classes for "inf" and "sup"

prove existence, uniqueness, and other properties of complex arg function

tuned

remove obsolete intermediate lemma complex_inverse_complex_split

tuned

merged

tuned

merged

merged

merged

merged

merged

tuned

merged

tuned

tuned

fixed computation of "in_conj" for polymorphic encodings

add some new lemmas about cis and rcis; simplify some proofs;

Complex.thy: move theorems into appropriate subsections

merged

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