isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

turn on "natural form" filtering in the Mirabelle tests, to see how it performs
2010-06-22, by blanchet
missing "Unsynchronized" + make exception take a unit
2010-06-22, by blanchet
added code to optionally perform fact filtering on the original (non-CNF) formulas
2010-06-22, by blanchet
more cosmetics
2010-06-22, by blanchet
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
2010-06-22, by blanchet
canonical argument order
2010-06-22, by blanchet
leverage new data structure for handling "add:" and "del:"
2010-06-22, by blanchet
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
2010-06-22, by blanchet
merge "generic_prover" and "generic_tptp_prover"
2010-06-22, by blanchet
removed Sledgehammer's support for the DFG syntax;
2010-06-22, by blanchet
distinguish between "unknown" and "no Kodkodi installed" errors
2010-06-22, by blanchet
reintroduce new Sledgehammer polymorphic handling code;
2010-06-22, by blanchet
make the Nitpick_Example theory processable even when Kodkodi is not installed;
2010-06-22, by blanchet
Make latex happy
2010-06-23, by hoelzl
Quotient package now uses Partial Equivalence instead place of equivalence
2010-06-23, by Cezary Kaliszyk
Replace 'list_rel' by 'list_all2'; they are equivalent.
2010-06-23, by Cezary Kaliszyk
Proper treatment of non-inherited mixins.
2010-06-22, by ballarin
merged
2010-06-22, by hoelzl
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
2010-06-21, by hoelzl
reredisable new polymorphic code
2010-06-22, by blanchet
merged
2010-06-21, by blanchet
beta-eta was too much, because it transformed SOME x. P x into Eps P, which caused problems later;
2010-06-21, by blanchet
back to post-release mode;
2010-06-21, by wenzelm
merged, resolving conflicts in doc-src/IsarRef/Thy/HOL_Specific.thy;
2010-06-21, by wenzelm
make Nitpick's unsound mode a bit more unsound
2010-06-21, by blanchet
sort cases on the proper key
2010-06-21, by blanchet
compile
2010-06-21, by blanchet
thread "full_types"
2010-06-21, by blanchet
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
2010-06-21, by blanchet
clean up after fcc768dc9dd0
2010-06-21, by blanchet
adjusted Nitpick examples to latest changes + make them slightly faster
2010-06-21, by blanchet
optimized code generated for datatype cases + more;
2010-06-21, by blanchet
activated Scala code generator test
2010-06-21, by haftmann
added bot instances; tuned
2010-06-21, by haftmann
extensionality rule fset_eqI
2010-06-21, by haftmann
merged
2010-06-20, by haftmann
separate section for diagnostic commands
2010-06-20, by haftmann
more binding; avoid arcane Rep and Abs prefixes
2010-06-19, by haftmann
cleanup of typecopy package
2010-06-19, by haftmann
quickcheck for fsets
2010-06-19, by haftmann
merged
2010-06-18, by nipkow
added pigeonhole lemmas
2010-06-18, by nipkow
merged
2010-06-18, by haftmann
tuned whitespace; dropped dead code
2010-06-18, by haftmann
code_simp: only succeed on real progress
2010-06-18, by haftmann
prefer fold over foldl
2010-06-18, by haftmann
conclude simplification with default simpset
2010-06-18, by haftmann
drop subsumed default equations (requires a little bit unfortunate laziness)
2010-06-18, by haftmann
avoid Scala legacy operations
2010-06-18, by haftmann
prefer fold over foldl
2010-06-18, by haftmann
made List.thy a join point in the theory graph
2010-06-18, by haftmann
tuned set_replicate lemmas
2010-06-18, by nipkow
merged
2010-06-18, by nipkow
added lemmas
2010-06-18, by nipkow
dropped dead code
2010-06-18, by haftmann
replaced unreliable metis proof
2010-06-17, by haftmann
rev is reverse in Haskell
2010-06-17, by haftmann
first serious draft of a scala code generator
2010-06-17, by haftmann
more precise code
2010-06-17, by haftmann
explicit type variable arguments for constructors
2010-06-17, by haftmann

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle