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 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 +30000 tip

simplified clasimpset declarations -- prefer attributes;
2011-05-13, by wenzelm
reduce the number of mono iterations to prevent the mono code from going berserk
2011-05-13, by blanchet
tuned comment
2011-05-13, by blanchet
optimized a common case
2011-05-13, by blanchet
avoid "UnequalLengths" exception for special constant "fequal" -- and optimize code in the common case where no type arguments are needed
2011-05-13, by blanchet
tweak E slices
2011-05-13, by blanchet
make SML/NJ happy
2011-05-13, by blanchet
fixed off-by-one bug
2011-05-13, by blanchet
added convenience syntax
2011-05-13, by blanchet
prefer Proof.context over old-style claset/simpset;
2011-05-12, by wenzelm
prefer plain simpset operations;
2011-05-12, by wenzelm
removed obsolete old-style cs/css;
2011-05-12, by wenzelm
modernized dead code;
2011-05-12, by wenzelm
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
2011-05-12, by wenzelm
eliminated obsolete MI_css -- use current context directly;
2011-05-12, by wenzelm
proper method_setup;
2011-05-12, by wenzelm
modernized simproc_setup;
2011-05-12, by wenzelm
prefer Proof.context over old-style clasimpset;
2011-05-12, by wenzelm
modernized dead code;
2011-05-12, by wenzelm
modernized specifications;
2011-05-12, by wenzelm
merged
2011-05-12, by wenzelm
added hints and FAQs
2011-05-12, by blanchet
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
2011-05-12, by blanchet
fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP
2011-05-12, by blanchet

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

isabelle