2010-09-03 ago wenzelm more explicit Config.declare vs. Config.declare_global;
2010-09-03 ago wenzelm turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;
2010-09-03 ago blanchet remove code I submitted accidentally
2010-09-03 ago blanchet merged
2010-09-03 ago blanchet disable "definitional CNF";
2010-09-03 ago blanchet redisable Nitpick from Cygwin, until I've investigated the issue
2010-09-02 ago blanchet show the number of facts for each prover in "verbose" mode
2010-09-02 ago blanchet fix bug in "debug" mode
2010-09-02 ago blanchet make sure "Unknown ATP" errors reach the users -- i.e. don't generate them from a thread
2010-09-02 ago blanchet If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
2010-09-02 ago blanchet fix trivial "x = x" fact detection
2010-09-03 ago wenzelm merged
2010-09-03 ago haftmann merged
2010-09-02 ago haftmann merged
2010-09-02 ago haftmann hand out deresolver from serializer invocation
2010-09-02 ago hoelzl Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)
2010-09-02 ago hoelzl merged
2010-09-02 ago hoelzl Updated proofs in Dining Cryptographers theory
2010-09-02 ago hoelzl Corrected definition and hence removed sorry.
2010-09-02 ago hoelzl Moved lemmas to appropriate locations
2010-09-02 ago hoelzl merged
2010-09-02 ago hellerar merged
2010-09-02 ago hellerar measure unique
2010-09-01 ago hellerar merge
2010-09-02 ago hoelzl move lemmas to correct theory files
2010-08-27 ago hoelzl factorizable measurable functions
2010-08-27 ago hoelzl Introduced sigma algebra generated by function preimages.
2010-08-27 ago hoelzl vimage of measurable function is a measure space
2010-08-27 ago hoelzl Measurable on product space is equiv. to measurable components
2010-08-27 ago hoelzl Measurable on euclidean space is equiv. to measurable components
2010-08-27 ago hoelzl preimages of open sets over continuous function are open
2010-08-27 ago hoelzl added definition of conditional expectation
2010-08-27 ago hoelzl proved existence of conditional expectation
2010-08-26 ago hoelzl introduced integration on subalgebras
2010-08-26 ago hoelzl changed definition of dynkin; replaces proofs by metis calles
2010-08-26 ago hellerar dynkin
2010-08-26 ago hellerar dynkin system
2010-09-02 ago hoelzl merged
2010-09-02 ago hoelzl Fixes lemma names
2010-09-02 ago hoelzl NEWS
2010-09-02 ago hoelzl Introduce surj_on and replace surj and bij by abbreviations.
2010-09-02 ago hoelzl Permutation implies bij function
2010-09-02 ago hoelzl bij <--> bij_betw
2010-09-02 ago hoelzl Add filter_remove1
2010-09-02 ago hoelzl Add lessThan_Suc_eq_insert_0
2010-09-02 ago haftmann merged
2010-09-02 ago haftmann updated
2010-09-02 ago haftmann set printmode while marking
2010-09-02 ago haftmann updated
2010-09-02 ago haftmann avoid reference to theory Ferrack altogether
2010-09-02 ago haftmann more canonical theory setup
2010-09-02 ago haftmann set depth to 1
2010-09-02 ago haftmann avoid theory Imperative_HOL altogether
2010-09-02 ago haftmann adapted to change eq -> equal
2010-09-02 ago haftmann corrected printmode handling
2010-09-02 ago haftmann swapped slip
2010-09-02 ago haftmann updated
2010-09-02 ago haftmann restored and added surpression of case combinators
2010-09-02 ago haftmann dropped superfluous presentation names
2010-09-02 ago haftmann manage statement selection for presentation wholly through markup