Mercurialisabelle / shortlog
summary | shortlog | changelog | graph | tags | branches | files | gz
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 tip
 
3 months ago blanchet 2012-02-11 new SPASS options changeset | files
3 months ago bulwahn 2012-02-11 making num_mutations a configuration that can be changed with the mutabelle bash command changeset | files
3 months ago bulwahn 2012-02-11 making max_mutants an option that can be changed in the Mutabelle-script changeset | files
3 months ago bulwahn 2012-02-11 increase timeout to 30 seconds; changing mutabelle script changeset | files
3 months ago blanchet 2012-02-10 parse clauses generated from several formulas changeset | files
3 months ago blanchet 2012-02-10 be more gentle when generating KBO weights changeset | files
3 months ago blanchet 2012-02-10 update SPASS slices changeset | files
3 months ago Cezary Kaliszyk 2012-02-10 more specification of the quotient package in IsarRef changeset | files
3 months ago Cezary Kaliszyk 2012-02-10 specification of the quotient package changeset | files
3 months ago blanchet 2012-02-09 tune KBO weight code changeset | files
3 months ago blanchet 2012-02-09 minor DFG fix changeset | files
3 months ago blanchet 2012-02-09 new SPASS slices changeset | files
3 months ago blanchet 2012-02-09 improved KBO weights -- beware of explicit applications changeset | files
3 months ago blanchet 2012-02-09 added possibility of generating KBO weights to DFG problems changeset | files
3 months ago Cezary Kaliszyk 2012-02-09 Generalize the compositional preservation theorems changeset | files
3 months ago blanchet 2012-02-08 use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules") changeset | files
3 months ago blanchet 2012-02-08 removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly changeset | files
3 months ago blanchet 2012-02-08 beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms changeset | files
3 months ago blanchet 2012-02-06 fixed arity error changeset | files
3 months ago blanchet 2012-02-06 tuning changeset | files
3 months ago blanchet 2012-02-06 renamed type encoding changeset | files
3 months ago bulwahn 2012-02-05 adding some forbidden constant names for mutabelle changeset | files
3 months ago bulwahn 2012-02-05 mutabelle ignores theorems with internal constants changeset | files
3 months ago nipkow 2012-02-05 tuned changeset | files
3 months ago nipkow 2012-02-05 merged changeset | files
3 months ago nipkow 2012-02-05 simplified code generation changeset | files
3 months ago blanchet 2012-02-05 remove option that's on by default changeset | files
3 months ago blanchet 2012-02-05 no need for a script/mega-hack with the new SPASS changeset | files
3 months ago blanchet 2012-02-05 cleaned up new SPASS parsing changeset | files
3 months ago blanchet 2012-02-05 tuning changeset | files
3 months ago bulwahn 2012-02-05 merged changeset | files
3 months ago bulwahn 2012-02-05 adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists changeset | files
3 months ago bulwahn 2012-02-05 tuning to remove ML warnings changeset | files
3 months ago blanchet 2012-02-05 removed double filtering of type args changeset | files
3 months ago bulwahn 2012-02-05 adding a quickcheck example about functions and sets changeset | files
3 months ago bulwahn 2012-02-05 removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since) changeset | files
3 months ago bulwahn 2012-02-05 adding a remark about lemma which is too special and should be removed changeset | files
3 months ago bulwahn 2012-02-05 another try to improve code generation of set equality (cf. da32cf32c0c7) changeset | files
3 months ago bulwahn 2012-02-05 beautifying definitions of check_all and adding instance for finite_4 changeset | files
3 months ago Cezary Kaliszyk 2012-02-05 Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients. changeset | files
3 months ago blanchet 2012-02-04 added option to Mirabelle/Sledgehammer changeset | files
3 months ago blanchet 2012-02-04 improved hashing w.r.t. Mirabelle, to help debugging changeset | files
3 months ago blanchet 2012-02-04 tuned SPASS DFG output changeset | files
3 months ago blanchet 2012-02-04 the new SPASS gives accurate fact information, so no need for old hack anymore changeset | files
3 months ago blanchet 2012-02-04 fixed docs changeset | files
3 months ago blanchet 2012-02-04 made sure to filter type args also for "uncurried alias" equations changeset | files
3 months ago blanchet 2012-02-04 made option available to users (mostly for experiments) changeset | files
3 months ago bulwahn 2012-02-04 using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a) changeset | files
3 months ago blanchet 2012-02-03 optimization: slice caching in case two consecutive slices are nearly identical changeset | files
3 months ago blanchet 2012-02-03 extended SPASS/DFG output with ranks changeset | files
3 months ago blanchet 2012-02-03 try to pass fewer options to Metis changeset | files
3 months ago Cezary Kaliszyk 2012-02-03 Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat changeset | files
3 months ago blanchet 2012-02-02 improve SPASS scripts changeset | files
3 months ago blanchet 2012-02-02 change 9ce354a77908 wasn't quite right -- here's an improvement changeset | files
3 months ago blanchet 2012-02-02 better SPASS setup changeset | files
3 months ago blanchet 2012-02-02 don't introduce new symbols in helpers -- makes problems unprovable changeset | files
3 months ago blanchet 2012-02-02 only constants can be aliased changeset | files
3 months ago blanchet 2012-02-02 include new SPASS by default if available changeset | files
3 months ago bulwahn 2012-02-02 adding an example for finite and cofinite sets changeset | files
3 months ago bulwahn 2012-02-02 adding a minimally refined equality on sets for code generation changeset | files
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 tip
isabelle