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

added "isabelle scalac" convenience;
2011-09-17, by wenzelm
Symbol.explode as in ML;
2011-09-17, by wenzelm
ignore OUTPUT to avoid spam -- jEdit menu "Troubleshooting / Activity Log" should be sufficient;
2011-09-17, by wenzelm
dropped unused argument – avoids problem with SML/NJ
2011-09-17, by haftmann
tuned spacing
2011-09-17, by haftmann
tuned
2011-09-17, by haftmann
tuned post fixpoint setup
2011-09-17, by nipkow
merged
2011-09-17, by nipkow
when applying induction rules, remove names of assumptions that come
2011-09-16, by nipkow
remove stray "using [[simp_trace]]"
2011-09-16, by noschinl
tune indenting
2011-09-16, by noschinl
removed unused legacy lemma names, some comment cleanup.
2011-09-16, by kleing
removed word_neq_0_conv from simpset, it's almost never wanted.
2011-09-16, by kleing
removed further legacy rules from Complete_Lattices
2011-09-15, by hoelzl
NEWS on Complete_Lattices, Lattices
2011-09-15, by noschinl
tail recursive proof preprocessing (needed for huge proofs)
2011-09-15, by blanchet
tuning
2011-09-15, by blanchet
merged
2011-09-15, by nipkow
revised AbsInt and added widening and narrowing
2011-09-15, by nipkow
updated comment
2011-09-14, by haftmann
updated generated code
2011-09-14, by haftmann
tuned
2011-09-13, by haftmann
renamed Complete_Lattices lemmas, removed legacy names
2011-09-14, by hoelzl
merged
2011-09-14, by noschinl
create central list for language extensions used by the haskell code generator
2011-09-14, by noschinl
observe distinction between sets and predicates
2011-09-14, by boehmes
merged
2011-09-14, by nipkow
cleand up AbsInt fixpoint iteration; tuned syntax
2011-09-14, by nipkow
tuned proofs
2011-09-13, by huffman
tuned proofs
2011-09-13, by huffman
remove some redundant [simp] declarations;
2011-09-13, by huffman
tune proofs
2011-09-13, by noschinl
tune simpset for Complete_Lattices
2011-09-13, by noschinl
merged
2011-09-13, by bulwahn
added lemma motivated by a more specific lemma in the AFP-KBPs theories
2011-09-13, by bulwahn
simplified unsound proof detection by removing impossible case
2011-09-13, by blanchet
correcting NEWS
2011-09-13, by bulwahn
correcting theory name and dependencies
2011-09-13, by bulwahn
renamed AList_Impl to AList
2011-09-13, by bulwahn
fastsimp -> fastforce in doc
2011-09-13, by nipkow
fix typo
2011-09-12, by huffman
shorten proof of frontier_straddle
2011-09-12, by huffman
NEWS and CONTRIBUTORS
2011-09-12, by huffman
remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
2011-09-12, by huffman
simplify proofs using LIMSEQ lemmas
2011-09-12, by huffman
remove trivial lemma Lim_at_iff_LIM
2011-09-12, by huffman
fix typos
2011-09-12, by huffman
NEWS for euclidean_space class
2011-09-12, by huffman
move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
2011-09-12, by huffman
adding NEWS and CONTRIBUTORS
2011-09-12, by hoelzl
merged
2011-09-12, by bulwahn
correcting imports after splitting and renaming AssocList
2011-09-12, by bulwahn
tuned
2011-09-12, by bulwahn
moving connection of association lists to Mappings into a separate theory
2011-09-12, by bulwahn
adding NEWS and CONTRIBUTORS
2011-09-12, by bulwahn
tuned some symbol that probably went there by some strange encoding issue
2011-09-12, by bulwahn
added my contributions to NEWS and CONTRIBUTORS
2011-09-12, by blanchet
fixed type intersection (again)
2011-09-12, by blanchet
consistent option naming
2011-09-12, by blanchet
NEWS fastsimp -> fastforce
2011-09-12, by nipkow
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