isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

new fastforce replacing fastsimp - less confusing name
2011-09-12, by nipkow
merged
2011-09-11, by wenzelm
NEWS for Library/Product_Lattice.thy
2011-09-11, by huffman
misc tuning and clarification;
2011-09-11, by wenzelm
merged
2011-09-11, by wenzelm
merged
2011-09-11, by huffman
tuned proofs
2011-09-11, by huffman
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
2011-09-11, by huffman
more CONTRIBUTORS;
2011-09-11, by wenzelm
persistent ISABELLE_INTERFACE_CHOICE;
2011-09-11, by wenzelm
explicit choice of interface;
2011-09-11, by wenzelm
more orthogonal signature;
2011-09-11, by wenzelm
updates for release;
2011-09-11, by wenzelm
misc tuning and clarification (NB: settings are already local for named snapshots/releases);
2011-09-11, by wenzelm
some updates of PLATFORMS;
2011-09-11, by wenzelm
more README;
2011-09-11, by wenzelm
merged
2011-09-10, by wenzelm
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
2011-09-10, by krauss
misc tuning;
2011-09-10, by wenzelm
misc tuning and clarification;
2011-09-10, by wenzelm
speed up slow proof;
2011-09-10, by wenzelm
merged
2011-09-10, by wenzelm
more modularization
2011-09-10, by haftmann
stronger colors (as background);
2011-09-10, by wenzelm
some color scheme for theory status;
2011-09-10, by wenzelm
some keyboard shortcuts for important actions;
2011-09-10, by wenzelm
explicit jEdit actions -- to enable key mappings, for example;
2011-09-10, by wenzelm
more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
2011-09-10, by wenzelm
tuned usage;
2011-09-10, by wenzelm
simplified default Isabelle application wrapper (NB: build process is already part of isabelle jedit tool);
2011-09-10, by wenzelm
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
2011-09-10, by haftmann
fixed definition of type intersection (soundness bug)
2011-09-10, by blanchet
continue with minimization in debug mode in spite of unsoundness
2011-09-10, by blanchet
generalize lemma of_nat_number_of_eq to class number_semiring
2011-09-09, by huffman
merged
2011-09-09, by bulwahn
stating more explicitly our expectation that these two terms have the same term structure
2011-09-09, by bulwahn
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
2011-09-09, by bulwahn
made SML/NJ happy
2011-09-09, by blanchet
call ghc with -XEmptyDataDecls
2011-09-08, by noschinl
merged
2011-09-09, by nipkow
tuned headers
2011-09-09, by nipkow
Library/Saturated.thy: number_semiring class instance
2011-09-08, by huffman
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
2011-09-08, by huffman
merged
2011-09-08, by huffman
remove unnecessary intermediate lemmas
2011-09-08, by huffman
added syntactic classes for "inf" and "sup"
2011-09-09, by krauss
prove existence, uniqueness, and other properties of complex arg function
2011-09-08, by huffman
tuned
2011-09-08, by huffman
remove obsolete intermediate lemma complex_inverse_complex_split
2011-09-08, by huffman
tuned
2011-09-08, by huffman
merged
2011-09-08, by haftmann
tuned
2011-09-08, by haftmann
merged
2011-09-08, by haftmann
merged
2011-09-07, by haftmann
merged
2011-09-06, by haftmann
merged
2011-09-06, by haftmann
merged
2011-09-06, by haftmann
tuned
2011-09-05, by haftmann
merged
2011-09-05, by haftmann
tuned
2011-09-05, by haftmann
tuned
2011-09-04, by haftmann
fixed computation of "in_conj" for polymorphic encodings
2011-09-08, by blanchet
add some new lemmas about cis and rcis;
2011-09-07, by huffman
Complex.thy: move theorems into appropriate subsections
2011-09-07, by huffman
merged
2011-09-07, by huffman
remove redundant lemma complex_of_real_minus_one
2011-09-07, by huffman
simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
2011-09-07, by huffman
removed unused lemma sin_cos_squared_add2_mult
2011-09-07, by huffman
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
2011-09-07, by huffman
avoid using legacy theorem names
2011-09-07, by huffman
merged
2011-09-08, by wenzelm
theory of saturated naturals contributed by Peter Gammie
2011-09-07, by haftmann
theory of saturated naturals contributed by Peter Gammie
2011-09-07, by haftmann
lemmas about +, *, min, max on nat
2011-09-07, by haftmann
update Sledgehammer docs
2011-09-07, by blanchet
added new tagged encodings to Metis tests
2011-09-07, by blanchet
also implemented ghost version of the tagged encodings
2011-09-07, by blanchet
added new guards encoding to test
2011-09-07, by blanchet
smarter explicit apply business
2011-09-07, by blanchet
started work on ghost type arg encoding
2011-09-07, by blanchet
stricted type encoding parsing
2011-09-07, by blanchet
more substructural sharing to gain significant compression;
2011-09-08, by wenzelm
XML.cache for partial sharing (strings only);
2011-09-07, by wenzelm
platform-specific look and feel;
2011-09-07, by wenzelm
more README;
2011-09-07, by wenzelm
clarified terminology;
2011-09-07, by wenzelm
no print_state for final proof commands, which return to theory state;
2011-09-07, by wenzelm
NEWS on IsabelleText font;
2011-09-07, by wenzelm
explicit join_syntax ensures command transaction integrity of 'theory';
2011-09-07, by wenzelm
some updates for release;
2011-09-07, by wenzelm
some tuning for release;
2011-09-07, by wenzelm
updated file locations;
2011-09-07, by wenzelm
merged
2011-09-07, by wenzelm
merged
2011-09-07, by bulwahn
removing previously used function locally_monomorphic in the code generator
2011-09-07, by bulwahn
setting const_sorts to false in the type inference of the code generator
2011-09-07, by bulwahn
adapting Imperative HOL serializer to changes of the iterm datatype in the code generator
2011-09-07, by bulwahn
removing previous crude approximation to add type annotations to disambiguate types
2011-09-07, by bulwahn
adding minimalistic implementation for printing the type annotations
2011-09-07, by bulwahn
adding call to disambiguation annotations
2011-09-07, by bulwahn
adding type inference for disambiguation annotations in code equation
2011-09-07, by bulwahn
adding the body type as well to the code generation for constants as it is required for type annotations of constants
2011-09-07, by bulwahn
changing const type to pass along if typing annotations are necessary for disambigous terms
2011-09-07, by bulwahn
fixed THF type constructor syntax
2011-09-07, by blanchet
tweaking polymorphic TFF and THF output
2011-09-07, by blanchet
parse new experimental '@' encodings
2011-09-07, by blanchet
tuning
2011-09-07, by blanchet
tuning
2011-09-07, by blanchet
tuning
2011-09-07, by blanchet
clarified import;
2011-09-07, by wenzelm
tuned/simplified proofs;
2011-09-07, by wenzelm
tuned proofs;
2011-09-07, by wenzelm
deactivate unfinished charset provider for now, to avoid user confusion;
2011-09-07, by wenzelm
more NEWS;
2011-09-07, by wenzelm
added "check" button: adhoc change to full buffer perspective;
2011-09-07, by wenzelm
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
2011-09-07, by wenzelm
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, by blanchet
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
2011-09-07, by blanchet
tuning
2011-09-07, by blanchet
make mangling sound w.r.t. type arguments
2011-09-07, by blanchet