| Wed, 10 Feb 2010 17:05:40 +0100 |
berghofe |
merged
|
changeset |
files
|
| Wed, 10 Feb 2010 17:05:18 +0100 |
berghofe |
Fixed bug in code for guessing the name of the variable representing the freshness context.
|
changeset |
files
|
| Wed, 10 Feb 2010 15:52:12 +0100 |
haftmann |
dropped last occurence of the linlinordered accident
|
changeset |
files
|
| Wed, 10 Feb 2010 15:14:06 +0100 |
haftmann |
dropped Id
|
changeset |
files
|
| Wed, 10 Feb 2010 15:14:01 +0100 |
haftmann |
minor metis proof tuning
|
changeset |
files
|
| Wed, 10 Feb 2010 14:12:40 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 10 Feb 2010 14:12:30 +0100 |
haftmann |
NEWS
|
changeset |
files
|
| Wed, 10 Feb 2010 14:12:04 +0100 |
haftmann |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
changeset |
files
|
| Wed, 10 Feb 2010 14:12:02 +0100 |
haftmann |
revert uninspired Structure_Syntax experiment
|
changeset |
files
|
| Wed, 10 Feb 2010 14:12:02 +0100 |
haftmann |
moved lemma field_le_epsilon from Real.thy to Fields.thy
|
changeset |
files
|
| Wed, 10 Feb 2010 12:04:57 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 10 Feb 2010 12:03:13 +0100 |
wenzelm |
unset KODKODI explicitly -- apparently isatest patches settings cumulatively;
|
changeset |
files
|
| Wed, 10 Feb 2010 11:47:33 +0100 |
blanchet |
make Nitpick test a bit weaker;
|
changeset |
files
|
| Wed, 10 Feb 2010 08:54:56 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 10 Feb 2010 08:54:40 +0100 |
haftmann |
moved constants inverse and divide to Ring.thy
|
changeset |
files
|
| Wed, 10 Feb 2010 08:49:26 +0100 |
haftmann |
moved constants inverse and divide to Ring.thy
|
changeset |
files
|
| Wed, 10 Feb 2010 08:49:26 +0100 |
haftmann |
division ring assumes divide_inverse
|
changeset |
files
|
| Wed, 10 Feb 2010 08:49:25 +0100 |
haftmann |
rely less on ordered rewriting
|
changeset |
files
|
| Wed, 10 Feb 2010 00:51:54 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 09 Feb 2010 21:32:57 +0100 |
blanchet |
merged
|
changeset |
files
|
| Tue, 09 Feb 2010 17:06:05 +0100 |
blanchet |
merged (manual for "nitpick_hol.ML" and "kodkod.ML")
|
changeset |
files
|
| Tue, 09 Feb 2010 16:07:51 +0100 |
blanchet |
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
|
changeset |
files
|
| Tue, 09 Feb 2010 16:05:49 +0100 |
blanchet |
make Quickcheck identify itself, so people don't submit bug reports to me thinking that it was Nitpick
|
changeset |
files
|
| Fri, 05 Feb 2010 14:27:21 +0100 |
blanchet |
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
|
changeset |
files
|