2010-02-11 wenzelm 2010-02-11 modernized syntax/translations;
2010-02-11 wenzelm 2010-02-11 modernized syntax/translations; tuned headers;
2010-02-11 wenzelm 2010-02-11 modernized translations;
2010-02-11 boehmes 2010-02-11 merged
2010-02-11 boehmes 2010-02-11 use full paths when importing theories
2010-02-11 nipkow 2010-02-11 merged
2010-02-11 nipkow 2010-02-11 inductive vs inductive_set explanation
2010-02-11 wenzelm 2010-02-11 modernized translations;
2010-02-10 wenzelm 2010-02-10 modernized translations;
2010-02-10 wenzelm 2010-02-10 renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
2010-02-10 berghofe 2010-02-10 merged
2010-02-10 berghofe 2010-02-10 Fixed bug in code for guessing the name of the variable representing the freshness context.
2010-02-10 haftmann 2010-02-10 dropped last occurence of the linlinordered accident
2010-02-10 haftmann 2010-02-10 dropped Id
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