2010-02-10 haftmann 2010-02-10 minor metis proof tuning
2010-02-10 haftmann 2010-02-10 merged
2010-02-10 haftmann 2010-02-10 NEWS
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-10 haftmann 2010-02-10 revert uninspired Structure_Syntax experiment
2010-02-10 haftmann 2010-02-10 moved lemma field_le_epsilon from Real.thy to Fields.thy
2010-02-10 wenzelm 2010-02-10 merged
2010-02-10 wenzelm 2010-02-10 unset KODKODI explicitly -- apparently isatest patches settings cumulatively;
2010-02-10 blanchet 2010-02-10 make Nitpick test a bit weaker; this should solve failure observed last night on "mac-poly"
2010-02-10 haftmann 2010-02-10 merged
2010-02-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
2010-02-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
2010-02-10 haftmann 2010-02-10 division ring assumes divide_inverse
2010-02-10 haftmann 2010-02-10 rely less on ordered rewriting
2010-02-10 wenzelm 2010-02-10 merged
2010-02-09 blanchet 2010-02-09 merged
2010-02-09 blanchet 2010-02-09 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
2010-02-09 blanchet 2010-02-09 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
2010-02-09 blanchet 2010-02-09 make Quickcheck identify itself, so people don't submit bug reports to me thinking that it was Nitpick
2010-02-05 blanchet 2010-02-05 added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
2010-02-05 blanchet 2010-02-05 handle Nitpick's nonstandard model enumeration in a cleaner way; and renumber the atoms so that we get more often a_1 and a_2 and less often a_{n-1} and a_{n-2} in counterexamples
2010-02-05 blanchet 2010-02-05 proper quoting of file paths when invoking Kodkodi from Nitpick
2010-02-05 blanchet 2010-02-05 merged
2010-02-05 blanchet 2010-02-05 optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil"; this gains one cardinality in the AA tree examples in the Nitpick manual
2010-02-04 blanchet 2010-02-04 adapted example following previous Nitpick change and fixed minor optimization in Nitpick
2010-02-04 blanchet 2010-02-04 split "nitpick_hol.ML" into two files to make it more manageable; more refactoring to come
2010-02-10 wenzelm 2010-02-10 removed obsolete CVS Ids;
2010-02-10 wenzelm 2010-02-10 modernized translations;
2010-02-10 wenzelm 2010-02-10 modernized syntax translations, using mostly abbreviation/notation; minor tuning;
2010-02-09 haftmann 2010-02-09 simple proofs make life faster and easier
2010-02-09 haftmann 2010-02-09 merged
2010-02-09 haftmann 2010-02-09 hide fact names clashing with fact names from Group.thy
2010-02-09 haftmann 2010-02-09 dropped lemma duplicates
2010-02-09 wenzelm 2010-02-09 isatest: activated HOL-Nitpick_Examples (by adding component kodkodi) on some platforms where it mostly works as expected;
2010-02-09 haftmann 2010-02-09 adjusted to cs. 9f841f20dca6
2010-02-08 huffman 2010-02-08 merged
2010-02-08 huffman 2010-02-08 correct definedness side conditions for copy_apps and take_apps
2010-02-08 huffman 2010-02-08 handle case where copy_stricts cannot be proven; rewrite proof script for take_apps
2010-02-07 huffman 2010-02-07 rewrite proof script for take_stricts
2010-02-07 huffman 2010-02-07 remove redundant theorem attributes
2010-02-07 huffman 2010-02-07 add lemma iterate_below_fix
2010-02-08 wenzelm 2010-02-08 modernized some syntax translations;
2010-02-08 wenzelm 2010-02-08 more precise dependencies;
2010-02-08 haftmann 2010-02-08 merged
2010-02-08 haftmann 2010-02-08 re-generated certificates
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-08 haftmann 2010-02-08 tuned spelling
2010-02-08 haftmann 2010-02-08 tuned proofs
2010-02-08 haftmann 2010-02-08 hide fact Nat.add_0_right; make add_0_right from Groups priority
2010-02-08 haftmann 2010-02-08 tuned header
2010-02-08 haftmann 2010-02-08 using code antiquotation
2010-02-08 haftmann 2010-02-08 tuned header
2010-02-08 haftmann 2010-02-08 dropped accidental duplication of "lin" prefix from cs. 108662d50512
2010-02-08 haftmann 2010-02-08 NEWS: ax_simps
2010-02-08 haftmann 2010-02-08 avoid upto in generated code (is infix operator in library.ML)
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
2010-02-08 haftmann 2010-02-08 merged
2010-02-08 haftmann 2010-02-08 more precise proofs
2010-02-08 haftmann 2010-02-08 moved auxiliary lemmas to more appropriate places
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures; more simp rules