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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
slightly changing the enumeration scheme
2012-02-25, by bulwahn
adding some more test invocations of find_unused_assms
2012-02-25, by bulwahn
adding an example where random beats exhaustive testing
2012-02-25, by bulwahn
removing unnecessary assumptions in RComplete;
2012-02-25, by bulwahn
removing unnecessary assumptions in RealDef;
2012-02-25, by bulwahn
one general list_all2_update_cong instead of two special ones
2012-02-25, by bulwahn
tuned comments;
2012-02-25, by wenzelm
standard Graph instances;
2012-02-25, by wenzelm
clarified signature -- avoid oddities of Iterable like Iterator.map;
2012-02-25, by wenzelm
discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
2012-02-25, by wenzelm
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24, by haftmann
explicit is better than implicit
2012-02-24, by haftmann
dropped dead code
2012-02-24, by haftmann
prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
2012-02-24, by wenzelm
tuned imports;
2012-02-24, by wenzelm
tuned signature;
2012-02-24, by wenzelm
discontinued obsolete Graph.all_paths (last seen in 1524d69783d3 and AFP/80bbbdbfec62);
2012-02-24, by wenzelm
merged
2012-02-24, by wenzelm
remove ill-formed lemmas word_0_wi_Pls and word_m1_wi_Min
2012-02-24, by huffman
avoid using Int.succ_def in proofs
2012-02-24, by huffman
avoid using Int.succ or Int.pred in proofs
2012-02-24, by huffman
avoid using BIT_simps in proofs;
2012-02-24, by huffman
avoid using BIT_simps in proofs
2012-02-24, by huffman
updated stats according to src/HOL/IsaMakefile;
2012-02-24, by wenzelm
more precise clean target;
2012-02-24, by wenzelm
clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;
2012-02-24, by wenzelm
avoid using Int.Pls_def in proofs
2012-02-24, by huffman
remove ill-formed lemmas word_pred_0_Min and word_m1_Min
2012-02-24, by huffman
remove ill-formed lemma of_bl_no; adapt proofs
2012-02-24, by huffman
adapt lemma mask_lem to respect int/bin distinction
2012-02-24, by huffman
rephrase some slow "metis" calls
2012-02-24, by blanchet
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
2012-02-24, by blanchet
general solution to the arity bug that occasionally plagues Sledgehammer -- short story, lots of things go kaputt when a polymorphic symbol's arity in the translation is higher than the arity of the fully polymorphic HOL constant
2012-02-24, by blanchet
renamed 'try_methods' to 'try0'
2012-02-24, by blanchet
doc fixes (thanks to Nik)
2012-02-24, by blanchet
fixed arity bug with "If" helpers for "If" that returns a function
2012-02-24, by blanchet
given up disfruitful branch
2012-02-24, by haftmann
explicit remove of lattice notation
2012-02-24, by haftmann
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24, by haftmann
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-23, by haftmann
dropped dead code
2012-02-23, by haftmann
tuned isatest settings;
2012-02-23, by wenzelm
merged
2012-02-23, by wenzelm
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
2012-02-23, by haftmann
tuned whitespace
2012-02-23, by haftmann
tuned proof
2012-02-23, by haftmann
prefer actual syntax categories;
2012-02-23, by wenzelm
avoid trait Addable, which is deprecated in scala-2.9.x;
2012-02-23, by wenzelm
streamlined abstract datatype;
2012-02-23, by wenzelm
tuned;
2012-02-23, by wenzelm
streamlined abstract datatype;
2012-02-23, by wenzelm
tuned -- avoid copy of empty value;
2012-02-23, by wenzelm
tuned;
2012-02-23, by wenzelm
streamlined abstract datatype, eliminating odd representation class;
2012-02-23, by wenzelm
tuned;
2012-02-23, by wenzelm
merged
2012-02-23, by huffman
make more simp rules respect int/bin distinction
2012-02-23, by huffman
make bool list functions respect int/bin distinction
2012-02-23, by huffman
merged;
2012-02-23, by wenzelm
tuned;
2012-02-23, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip