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

enforce short hostname on all platforms (especially macbroy2);
2011-12-17, by wenzelm
clarified modules that contribute to datatype package;
2011-12-17, by wenzelm
tuned signature;
2011-12-17, by wenzelm
merged
2011-12-16, by wenzelm
merged
2011-12-16, by nipkow
improved indexed complete lattice
2011-12-16, by nipkow
more elementary defs;
2011-12-16, by wenzelm
eliminated old-fashioned Global_Theory.add_thms(s);
2011-12-16, by wenzelm
prefer sorting from Scala library;
2011-12-16, by wenzelm
prefer Name.context operations;
2011-12-16, by wenzelm
tuned;
2011-12-16, by wenzelm
clarified modules that contribute to datatype package;
2011-12-16, by wenzelm
tuned signature;
2011-12-16, by wenzelm
merged;
2011-12-15, by wenzelm
tuned;
2011-12-15, by wenzelm
add complementary lemmas for {min,max}_least
2011-12-15, by noschinl
add lemmas about limits
2011-12-15, by noschinl
clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
2011-12-15, by wenzelm
separate rep_datatype.ML;
2011-12-15, by wenzelm
misc tuning and simplification;
2011-12-15, by wenzelm
more stats;
2011-12-15, by wenzelm
made SML/NJ happier
2011-12-15, by blanchet
merged
2011-12-15, by nipkow
tuned
2011-12-15, by nipkow
hiding the precious name map_entry in AList_Impl
2011-12-15, by bulwahn
killed dead code
2011-12-14, by blanchet
use new redirection algorithm in Sledgehammer
2011-12-14, by blanchet
fixed parsing of TPTP atoms
2011-12-14, by blanchet
tuned signature;
2011-12-14, by wenzelm
avoid fragile Sign.intern_const -- pass internal names directly;
2011-12-14, by wenzelm
tuned;
2011-12-14, by wenzelm
added new proof redirection code
2011-12-14, by blanchet
SPASS is incomplete because of the -Splits and -FullRed options, not just because of -SOS=1 -- don't pretend the opposite
2011-12-14, by blanchet
make sure that all symbols are declared in untyped SPASS DFG output (broken since 3b8606fba2dd)
2011-12-14, by blanchet
NEWS
2011-12-14, by bulwahn
correcting dependencies after renaming
2011-12-14, by bulwahn
tuned header after renaming
2011-12-14, by bulwahn
moving AList theory to AList_Impl to make space for the association lists with invariant
2011-12-14, by bulwahn
merged
2011-12-14, by bulwahn
adding map_entry to AList theory
2011-12-14, by bulwahn
adding map_default to AList theory
2011-12-14, by bulwahn
fixed typo in theorem name in AList theory
2011-12-14, by bulwahn
adding code attribute to enable evaluation of equality on multisets
2011-12-14, by bulwahn
merged
2011-12-14, by wenzelm
updated Sledgehammer/SMT docs
2011-12-14, by blanchet
tuned signature;
2011-12-14, by wenzelm
eliminated dead code;
2011-12-14, by wenzelm
some full isatest runs, which include benchmark targets;
2011-12-14, by wenzelm
more visible benchmarks;
2011-12-14, by wenzelm
fixed Nitpick definition of "<" on "real"s
2011-12-14, by blanchet
replace 'lemmas' with 'lemma'
2011-12-14, by huffman
merged
2011-12-14, by huffman
more simp rules for sbintrunc
2011-12-13, by huffman
add simp rules for sbintrunc applied to numerals
2011-12-13, by huffman
replace many uses of 'lemmas' with explicit 'lemma'
2011-12-13, by huffman
add lemma bin_nth_zero
2011-12-13, by huffman
add simp rules for bintrunc applied to numerals
2011-12-13, by huffman
add simp rules for bin_rest and bin_last applied to numerals
2011-12-13, by huffman
add simp rules for bin_sign applied to numerals
2011-12-13, by huffman
add simp rules for BIT applied to numerals
2011-12-13, by huffman

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

isabelle