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

tuned proofs;
2012-09-28, by wenzelm
simplified simpset
2012-09-28, by blanchet
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
2012-09-28, by blanchet
tuned tactic
2012-09-28, by traytel
updated keywords using proper "isabelle update_keywords";
2012-09-28, by wenzelm
tuned tactic
2012-09-28, by traytel
tuned tactic
2012-09-28, by traytel
merge
2012-09-28, by blanchet
renamed ML file in preparation for next step
2012-09-28, by blanchet
killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"
2012-09-28, by blanchet
modernized example, exploiting "rep_compat" option
2012-09-28, by blanchet
compatibility option to use "rep_datatype"
2012-09-28, by blanchet
tuned message
2012-09-28, by blanchet
modernized example
2012-09-28, by blanchet
tuned tactics
2012-09-28, by traytel
second usage of const_typ
2012-09-28, by nipkow
new antiquotation const_typ
2012-09-28, by nipkow
tuned printing of _ in latex
2012-09-28, by nipkow
mk_readable_rsp_thm_eq is more robust now
2012-09-27, by kuncar
new get function for non-symmetric relator_eq & tuned
2012-09-27, by kuncar
merged
2012-09-27, by wenzelm
tuned tactic; got rid of substs_tac alias
2012-09-27, by traytel
use a nicer scheme to indexify names
2012-09-27, by blanchet
tuned tactic
2012-09-27, by traytel
type of the bound of a BNF depends at most on dead type variables
2012-09-27, by traytel
repaired signature
2012-09-27, by blanchet
lower the defaults for the number of bits, based on an example by Lukas Bulwahn
2012-09-27, by blanchet
modernized examples
2012-09-27, by blanchet
merged
2012-09-27, by nipkow
tuned
2012-09-27, by nipkow
operations to turn markup into XML;
2012-09-27, by wenzelm
removed obsolete org.w3c.dom operations;
2012-09-27, by wenzelm
eliminated obsolete HTML/CSS functionality;
2012-09-27, by wenzelm
removed obsolete Output1 dockable;
2012-09-27, by wenzelm
physical File.eq in conformance to Isabelle/ML;
2012-09-27, by wenzelm
tuned proofs;
2012-09-27, by wenzelm
tuned;
2012-09-27, by wenzelm
updated to consolidated SortedMap in scala-2.9.x;
2012-09-27, by wenzelm
partly ported "TreeFI" example to new syntax
2012-09-27, by blanchet
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
2012-09-27, by blanchet
tuned
2012-09-27, by nipkow
tuned
2012-09-27, by nipkow
merge
2012-09-27, by blanchet
modernized examples;
2012-09-27, by blanchet
some support for jEdit warmstart;
2012-09-26, by wenzelm
discontinued XML.cache experiment -- Poly/ML 5.5.0 RTS does online sharing better;
2012-09-26, by wenzelm
tuned message;
2012-09-26, by wenzelm
merged
2012-09-26, by wenzelm
disable parallel proofs for two big examples -- speeds up things and eliminates spurious Interrupt exceptions (to be investigated)
2012-09-26, by blanchet
got rid of other instance of shaky "Thm.generalize"
2012-09-26, by blanchet
tweaked theorem names (in particular, dropped s's)
2012-09-26, by blanchet
get rid of shaky "Thm.generalize"
2012-09-26, by blanchet
fixed "rels" + split them into injectivity and distinctness
2012-09-26, by blanchet
generate high-level "coinduct" and "strong_coinduct" properties
2012-09-26, by blanchet
added coinduction tactic
2012-09-26, by blanchet
generalized tactic a bit
2012-09-26, by blanchet
export "dtor_map_coinduct" theorems, since they're used in one example
2012-09-26, by blanchet
name tuning
2012-09-26, by blanchet
parameterized "subst_tac"
2012-09-26, by blanchet
generate high-level "maps", "sets", and "rels" properties
2012-09-26, by blanchet

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

isabelle