isabelle: Graph

tuning
2014-06-10, by blanchet
add type class instances for unit
2014-06-10, by Andreas Lochbihler
use 'where' clause for selector default value syntax
2014-06-10, by blanchet
tuning
2014-06-10, by blanchet
added List.union
2014-06-09, by nipkow
Sup/Inf on functions decoupled from complete_lattice.
2014-06-09, by nipkow
tuned data structure
2014-06-08, by haftmann
recovered level-free fishing for locale, accidentally lost in dce365931721
2014-06-08, by haftmann
tuned terminology: emphasize stack-like nature of nested local theories
2014-06-08, by haftmann
self-contained locale_declaration operation
2014-06-08, by haftmann
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
2014-06-08, by haftmann
tuned
2014-06-08, by haftmann
recovered structure of module, which got somehow convoluted due to incremental modifications
2014-06-08, by haftmann
re-unified approach towards class and locale consts, with refined terminology: foo_const_declaration denotes declaration for a particular logical layer, foo_const the full stack for a particular target
2014-06-08, by haftmann
revert effect of 63c7b29d29ac -- existing pervasive interpretation of class order for dvd etc. is too obstrusive at the moment
2014-06-08, by haftmann
less ad-hoc verision of educated guess: guess identity of declaration morphism wrt. canonical morphism rather than observing particular effects of declaration morphisms only;
2014-06-08, by haftmann
treat non-canonical interpretations of classes the same way as ordinary locale interpretations
2014-06-07, by haftmann
tuned
2014-06-07, by haftmann
avoid odd Named_Target.reinit altogether
2014-06-07, by haftmann
clarified terminology: toplevel is interwined with named targets in particular, not with local theories in general
2014-06-07, by haftmann
less baroque interface
2014-06-07, by haftmann
dropped obscure and unused ad-hoc before_exit hook for named targets
2014-06-06, by haftmann
added lemma
2014-06-06, by nipkow
mira: USER_HOME must exist for building JEdit documentation
2014-06-05, by noschinl
added lemmas
2014-06-06, by nipkow
sharpened criterion: bare named target is only at the bottom level
2014-06-05, by haftmann
tuned
2014-06-05, by haftmann
extended stream library
2014-06-05, by traytel
be more explicit: made sml/nj happy
2014-06-05, by haftmann
always refine interpretation morphism using canonical constant's definition theorem
2014-06-05, by haftmann
set USER_HOME to affect also ISABELLE_PATH et al
2014-06-04, by noschinl
merge
2014-06-03, by blanchet
updated SMT2 certificates
2014-06-03, by blanchet
tune
2014-06-03, by blanchet
disable hard-to-reconstruct Z3 feature
2014-06-03, by blanchet
new Z3 4.3.2 component, based on more recent repository version, and whose Mac binary was built on Mac OS X 10.7
2014-06-03, by blanchet
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
2014-06-03, by hoelzl
removed SMT weights -- their impact was very inconclusive anyway
2014-06-03, by blanchet
make SMT code less dependent on Z3 proofs
2014-06-03, by blanchet
tuning
2014-06-03, by blanchet
avoid division by 0
2014-06-02, by blanchet
formal treatment of dangling parameters for class abbrevs analogously to class consts
2014-06-02, by haftmann
explicit passing of params
2014-06-02, by haftmann
refactored Z3 to Isar proof construction code
2014-06-02, by blanchet
simplified counterexample handling
2014-06-02, by blanchet
split replay and proof parsing for Z3
2014-06-02, by blanchet
removed counterexample parser (obsolete and useless in practice)
2014-06-02, by blanchet
remove superfluous assumption
2014-06-02, by hoelzl
basic setup for zipperposition prover
2014-06-02, by fleury
document property 'sel_set'
2014-06-02, by desharna
generate 'sel_set' theorem for (co)datatypes
2014-06-02, by desharna
removed some spurious warnings in new (co)datatype package
2014-06-02, by blanchet
add option to keep duplicates, for more precise evaluation of relevance filters
2014-06-02, by blanchet
tuned whitespace
2014-06-02, by blanchet
definition in class: provide explicit auxiliary abbreviation carrying potential mixfix syntax in presence of dangling parameters
2014-06-01, by haftmann
tuned
2014-06-01, by haftmann
merged
2014-05-31, by boehmes
tuned
2014-05-31, by boehmes
more complete proof replay for Z3: support universally quantified rewrite steps
2014-05-31, by boehmes
postpone const declarations for nested context after canonical const declarations: keep const declarations stemming from interpretation together
2014-05-31, by haftmann
tuned
2014-05-31, by haftmann
explicit is better than implicit
2014-05-31, by haftmann
tuned names
2014-05-31, by haftmann
dropped accidental duplicate application of morphism
2014-05-31, by haftmann
generalizd measurability on restricted space; rule for integrability on compact sets
2014-05-30, by hoelzl
better support for restrict_space
2014-05-30, by hoelzl
must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
2014-05-30, by nipkow
merged
2014-05-30, by wenzelm
updated cygwin -- include perl_vendor for libwww-perl;
2014-05-30, by wenzelm
made 'Kuehlwein-style' be really like Python code, we now think
2014-05-30, by blanchet
make SML code closer to Python code when 'nb_kuehlwein_style' is true
2014-05-30, by blanchet
merge
2014-05-30, by blanchet
added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away
2014-05-30, by blanchet
introduce more powerful reindexing rules for big operators
2014-05-30, by hoelzl
merged
2014-05-30, by wenzelm
make double-sure that old popup is dismissed, before replacing it;
2014-05-30, by wenzelm
more robust bold_style, e.g. relevant for accidental \<^bold> before keyword;
2014-05-30, by wenzelm
added another way of invoking Python code, for experiments
2014-05-30, by blanchet
make SML naive Bayes closer to Python version
2014-05-30, by blanchet
tuned whitespace, to make datatype definitions slightly less intimidating
2014-05-30, by blanchet
more work on exporter
2014-05-30, by blanchet
got rid of 'linearize' option
2014-05-30, by blanchet
extend exporter with new versions of MaSh
2014-05-30, by blanchet
tuned
2014-05-30, by haftmann
tuned signature
2014-05-30, by haftmann
terminating code equations
2014-05-30, by haftmann
more direct passing of right-hand side
2014-05-29, by haftmann
even more uniform treatment of result after 95e5a633a18f
2014-05-29, by haftmann
Merge
2014-05-29, by paulson
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
2014-05-29, by paulson
removed Kleene_Algebra because of superior AFP entry; authors agreed
2014-05-29, by nipkow
typo
2014-05-29, by nipkow
uniform treatmen of result
2014-05-28, by haftmann
tuned variable names
2014-05-28, by haftmann
more generous max number of suggestions, for more safety
2014-05-28, by blanchet
changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)
2014-05-28, by blanchet