isabelle: Graph

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

Corrected definition and hence removed sorry.
2010-09-02, by hoelzl
Moved lemmas to appropriate locations
2010-09-02, by hoelzl
merged
2010-09-02, by hoelzl
merged
2010-09-02, by hellerar
measure unique
2010-09-02, by hellerar
merge
2010-09-01, by hellerar
move lemmas to correct theory files
2010-09-02, by hoelzl
factorizable measurable functions
2010-08-27, by hoelzl
Introduced sigma algebra generated by function preimages.
2010-08-27, by hoelzl
vimage of measurable function is a measure space
2010-08-27, by hoelzl
Measurable on product space is equiv. to measurable components
2010-08-27, by hoelzl
Measurable on euclidean space is equiv. to measurable components
2010-08-27, by hoelzl
preimages of open sets over continuous function are open
2010-08-27, by hoelzl
added definition of conditional expectation
2010-08-27, by hoelzl
proved existence of conditional expectation
2010-08-27, by hoelzl
introduced integration on subalgebras
2010-08-26, by hoelzl
changed definition of dynkin; replaces proofs by metis calles
2010-08-26, by hoelzl
dynkin
2010-08-26, by hellerar
dynkin system
2010-08-26, by hellerar
merged
2010-09-02, by hoelzl
Fixes lemma names
2010-09-02, by hoelzl
NEWS
2010-09-02, by hoelzl
Introduce surj_on and replace surj and bij by abbreviations.
2010-09-02, by hoelzl
Permutation implies bij function
2010-09-02, by hoelzl
bij <--> bij_betw
2010-09-02, by hoelzl
Add filter_remove1
2010-09-02, by hoelzl
Add lessThan_Suc_eq_insert_0
2010-09-02, by hoelzl
merged
2010-09-02, by haftmann
updated
2010-09-02, by haftmann
set printmode while marking
2010-09-02, by haftmann
updated
2010-09-02, by haftmann
avoid reference to theory Ferrack altogether
2010-09-02, by haftmann
more canonical theory setup
2010-09-02, by haftmann
set depth to 1
2010-09-02, by haftmann
avoid theory Imperative_HOL altogether
2010-09-02, by haftmann
adapted to change eq -> equal
2010-09-02, by haftmann
corrected printmode handling
2010-09-02, by haftmann
swapped slip
2010-09-02, by haftmann
updated
2010-09-02, by haftmann
restored and added surpression of case combinators
2010-09-02, by haftmann
dropped superfluous presentation names
2010-09-02, by haftmann
manage statement selection for presentation wholly through markup
2010-09-02, by haftmann
formal markup of generated code for statements
2010-09-02, by haftmann
removed namespace stuff from code_printer
2010-09-02, by haftmann
merged
2010-09-02, by blanchet
reenable Nitpick on Cygwin;
2010-09-02, by blanchet
merged;
2010-09-03, by wenzelm
Proof.pretty_state: print everything in the foreground context to give users a chance to configure options, e.g. via "using [[show_consts]]";
2010-09-03, by wenzelm
turned show_consts into proper configuration option;
2010-09-03, by wenzelm
prefer regular Proof.context over background theory;
2010-09-03, by wenzelm
just one refute.ML;
2010-09-02, by wenzelm
use existing Integer.pow, despite its slightly odd argument order;
2010-09-02, by wenzelm
tuned whitespace and indentation, emphasizing the logical structure of this long text;
2010-09-02, by wenzelm
inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;
2010-09-02, by wenzelm
Document_View: squiggly underline for messages;
2010-09-02, by wenzelm
added gfx_range convenience;
2010-09-02, by wenzelm
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
2010-09-02, by wenzelm
Position.Range: exclude singularity (again);
2010-09-02, by wenzelm
merged
2010-09-02, by wenzelm
merged
2010-09-02, by blanchet
FIXME -> TODO (nothing is broken)
2010-09-02, by blanchet
Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
2010-09-02, by blanchet
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
2010-09-02, by blanchet
make definitional CNF translation code more robust in the presence of existential quantifiers in the "literals"
2010-09-02, by blanchet
formal framework for presentation of selected statements
2010-09-02, by haftmann
merged
2010-09-02, by haftmann
Table.map replaces Table.map'
2010-09-02, by haftmann
dropped dead code; tuned
2010-09-02, by haftmann
include names need not be considered as reserved any longer
2010-09-02, by haftmann
skip empty name bunches; fill up trailing positions with NONEs
2010-09-02, by haftmann
use code_namespace module for SML and OCaml code
2010-09-02, by haftmann
Table.map replaces Table.map'
2010-09-02, by haftmann
avoid cyclic modules
2010-09-02, by haftmann
merged
2010-09-02, by haftmann
simultaneous modification of statements: statement names
2010-09-01, by haftmann
simultaneous modification of statements
2010-09-01, by haftmann
explicit modify_stmt parameter
2010-09-01, by haftmann
Graph.map, in analogy to Table.map
2010-09-01, by haftmann
replaced Table.map' by Table.map
2010-09-01, by haftmann
merged
2010-09-01, by haftmann
tuned
2010-09-01, by haftmann
generalized hierarchical data structure over statements
2010-09-01, by haftmann
merged
2010-09-02, by haftmann
normalization is allowed to solve True
2010-09-02, by haftmann
merged
2010-09-02, by blanchet
merged
2010-09-02, by blanchet
cosmetics
2010-09-02, by blanchet
SNARK doesn't like facts
2010-09-02, by blanchet
show real CPU time
2010-09-02, by blanchet
factor out code shared by all ATPs so that it's run only once
2010-09-01, by blanchet
handle all whitespace, not just ASCII 32
2010-09-01, by blanchet
speed up SPASS hack + output time information in "blocking" mode
2010-09-01, by blanchet
remove time information in output, since it's confusing anyway
2010-09-01, by blanchet
minor refactoring
2010-09-01, by blanchet
translate the axioms to FOF once and for all ATPs
2010-09-01, by blanchet
run relevance filter in a thread, to avoid blocking
2010-09-01, by blanchet
add dependency of "spass" script
2010-09-01, by blanchet
more elegant ML
2010-09-01, by blanchet
only kill ATP threads in nonblocking mode
2010-09-01, by blanchet
lower number of facts given to SInE
2010-09-01, by blanchet
share the relevance filter among the provers
2010-09-01, by blanchet
got rid of the "theory_relevant" option;
2010-09-01, by blanchet
generalize theorem argument parsing syntax
2010-09-01, by blanchet
support new option in Mirabelle
2010-09-01, by blanchet
fiddled with fudge factor (based on Mirabelle)
2010-09-01, by blanchet
give priority to assumptions in structured proofs
2010-09-01, by blanchet
introduce fudge factors to deal with "theory const"
2010-09-01, by blanchet
rename sledgehammer config attributes
2010-09-01, by blanchet
finish moving file
2010-09-01, by blanchet
move file
2010-08-31, by blanchet
finished renaming
2010-08-31, by blanchet
fix typo
2010-08-31, by blanchet