isabelle: Graph

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

merged
2016-09-18, by Lars Hupel
tuned
2016-09-18, by Lars Hupel
clarified notation: iterated quantifier is negated as one chunk;
2016-09-18, by wenzelm
tuned proofs;
2016-09-18, by wenzelm
tuned;
2016-09-18, by wenzelm
clarified notation;
2016-09-18, by wenzelm
support replicate_mset in multiset simproc
2016-09-18, by fleury
tuning multiset simproc
2016-09-18, by fleury
repair LaTeX dropout from f83ef97d8d7d
2016-09-17, by Lars Hupel
prefer abbreviation for trivial set conversion
2016-09-16, by haftmann
more lemmas
2016-09-16, by haftmann
merged
2016-09-16, by wenzelm
more symbols -- as in the printed document;
2016-09-16, by wenzelm
more symbols;
2016-09-16, by wenzelm
tuned proofs
2016-09-16, by Lars Hupel
misc updates;
2016-09-16, by wenzelm
merged
2016-09-16, by wenzelm
consolidate implicit use of gnutar, via somewhat fragile dynamic scoping within existing shell scripts;
2016-09-16, by wenzelm
merged
2016-09-16, by immler
Liminf/Limsup and filtermap
2016-09-15, by immler
benchmark doesn't need to build documents
2016-09-16, by Lars Hupel
benchmark profile runs on small worker now (6 cores)
2016-09-16, by Lars Hupel
merged
2016-09-16, by traytel
NEWS
2016-09-16, by traytel
merged
2016-09-16, by wenzelm
serious measurements require jobs = 1;
2016-09-16, by wenzelm
sessions that are relevant for routine timing measurements;
2016-09-16, by wenzelm
more uniform completion of short word: exclude single character prefix but include two chracter prefix (see also 31633e503c17);
2016-09-16, by wenzelm
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
2016-09-16, by hoelzl
new type for finite maps; use it in HOL-Probability
2016-09-15, by Lars Hupel
adapted to listsum -> sum_list
2016-09-15, by nipkow
merged
2016-09-15, by nipkow
renamed listsum -> sum_list, listprod ~> prod_list
2016-09-15, by nipkow
lots of new results about topology, affine dimension etc
2016-09-15, by paulson
Merge
2016-09-15, by paulson
simple new lemmas, mostly about sets
2016-09-15, by paulson
add add_eq_0_iff_both_eq_0 and zero_eq_add_iff_both_eq_0 to simp set
2016-09-15, by hoelzl
tuned;
2016-09-15, by wenzelm
merged
2016-09-14, by wenzelm
NEWS;
2016-09-14, by wenzelm
handle font-size events;
2016-09-14, by wenzelm
clarified GUI representation of replacement texts with zero or more abbrevs;
2016-09-14, by wenzelm
handle update events;
2016-09-14, by wenzelm
discontinued global etc/abbrevs;
2016-09-14, by wenzelm
added abbrevs panel;
2016-09-14, by wenzelm
tuned;
2016-09-14, by wenzelm
more robust;
2016-09-14, by wenzelm
maintain abbrevs in canonical reverse order;
2016-09-14, by wenzelm
tuned;
2016-09-14, by wenzelm
tuned;
2016-09-14, by wenzelm
ignore default output directory of 'build_stats' tool
2016-09-14, by Lars Hupel
don't expose internal construction in the coinduction rule for mutual coinductive predicates
2016-09-13, by traytel
union associates to the left
2016-09-13, by blanchet
reorganization, more funs and lemmas
2016-09-13, by nipkow
more lemmas
2016-09-13, by nipkow
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
2016-09-12, by blanchet
tuned;
2016-09-12, by wenzelm
tuned -- fewer warnings;
2016-09-12, by wenzelm
moved ML function
2016-09-12, by blanchet
NEWS
2016-09-12, by blanchet
strengthened tactic
2016-09-12, by blanchet
avoid warning triggered by code generator
2016-09-12, by blanchet
strengthened tactic
2016-09-12, by blanchet
prove 'set' property backward
2016-09-12, by blanchet
more robust multiset simproc
2016-09-12, by fleury
delete looping simp rule
2016-09-12, by fleury
merged
2016-09-12, by wenzelm
tuned proofs;
2016-09-12, by wenzelm
tuned proofs;
2016-09-11, by wenzelm
generalized code towards nonuniform (co)datatypes
2016-09-11, by blanchet
merged
2016-09-11, by nipkow
more simp rules
2016-09-11, by nipkow
strengthened tactics
2016-09-11, by blanchet
derive relator properties forward
2016-09-11, by blanchet
derive maps forward
2016-09-11, by blanchet
tuning
2016-09-11, by blanchet
tuning
2016-09-11, by blanchet
provide a mechanism for ensuring dead type variables occur in typedef if desired
2016-09-11, by blanchet
preserve order of dead variables
2016-09-11, by blanchet
tuning
2016-09-11, by blanchet
tuned proofs;
2016-09-11, by wenzelm
misc tuning and modernization;
2016-09-11, by wenzelm
misc tuning and modernization;
2016-09-11, by wenzelm
more simp
2016-09-10, by nipkow
msetsum -> set_mset, msetprod -> prod_mset
2016-09-09, by nipkow
More on balancing; renamed theory to Balance
2016-09-09, by nipkow
added lemmas
2016-09-09, by nipkow
option "checkpoint" helps to fine-tune global heap space management;
2016-09-08, by wenzelm
made it easier to catch 'empty datatype' exception
2016-09-08, by blanchet
export ML functions
2016-09-08, by blanchet
tuning
2016-09-08, by blanchet
minimal HTTP server;
2016-09-08, by wenzelm
merged
2016-09-07, by wenzelm
unfold_abs_def is enabled by default;
2016-09-07, by wenzelm
discontinued theory-local special syntax for lattice orderings
2016-09-07, by haftmann
keep locale lifting rules on the global level
2016-09-07, by haftmann
tuning
2016-09-07, by blanchet
exported ML functions + tuning
2016-09-07, by blanchet
refactoring
2016-09-07, by blanchet
refactoring
2016-09-07, by blanchet
refactoring
2016-09-07, by blanchet
tuned whitespace
2016-09-07, by blanchet
merged
2016-09-06, by wenzelm
more operations;
2016-09-06, by wenzelm
clarified proof: save 1-2s CPU time;
2016-09-06, by wenzelm
tuned;
2016-09-06, by wenzelm
strictly sequential abbrevs;
2016-09-06, by wenzelm
clarified obscure facts;
2016-09-05, by wenzelm
clarified modules;
2016-09-05, by wenzelm
clarified modules;
2016-09-05, by wenzelm
standardized alias;
2016-09-05, by wenzelm
export more ML functions
2016-09-06, by blanchet
generalized ML signature
2016-09-06, by blanchet
extended ML signature + refactored
2016-09-06, by blanchet
extended ML signature
2016-09-06, by blanchet
generalized code (subtly)
2016-09-06, by blanchet
tuned ML signature
2016-09-06, by blanchet
exported ML functions
2016-09-05, by blanchet
export ML function + tuning
2016-09-05, by blanchet
tuning multisets; more interpretations
2016-09-05, by fleury
clean argument of simp add
2016-09-05, by fleury
add_mset constructor in multisets
2016-09-05, by fleury
merged
2016-09-05, by wenzelm
more operations;
2016-09-05, by wenzelm
more operations;
2016-09-05, by wenzelm
support resource management;
2016-09-05, by wenzelm
clarified modules;
2016-09-05, by wenzelm
export more ML functions
2016-09-05, by blanchet