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