blanchet [Fri, 05 Feb 2010 12:04:54 +0100] rev 35072
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
blanchet [Fri, 05 Feb 2010 11:24:53 +0100] rev 35071
proper quoting of file paths when invoking Kodkodi from Nitpick
blanchet [Fri, 05 Feb 2010 11:15:16 +0100] rev 35070
merged
blanchet [Fri, 05 Feb 2010 11:14:34 +0100] rev 35069
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
blanchet [Thu, 04 Feb 2010 16:50:26 +0100] rev 35068
adapted example following previous Nitpick change and fixed minor optimization in Nitpick
blanchet [Thu, 04 Feb 2010 16:03:15 +0100] rev 35067
split "nitpick_hol.ML" into two files to make it more manageable;
more refactoring to come
haftmann [Tue, 09 Feb 2010 16:07:09 +0100] rev 35066
simple proofs make life faster and easier
haftmann [Tue, 09 Feb 2010 14:32:16 +0100] rev 35065
merged
haftmann [Tue, 09 Feb 2010 11:47:47 +0100] rev 35064
hide fact names clashing with fact names from Group.thy
haftmann [Tue, 09 Feb 2010 11:07:14 +0100] rev 35063
dropped lemma duplicates