Sat, 16 Apr 2011 12:46:18 +0200 | wenzelm | tuned signature, disentangled dependencies; | changeset | files |
Fri, 15 Apr 2011 15:33:57 +0200 | berghofe | Added command for associating user-defined types with SPARK types. | changeset | files |
Thu, 14 Apr 2011 15:04:42 +0200 | noschinl | turn YXML.parse_file into a fold | changeset | files |
Thu, 14 Apr 2011 11:24:05 +0200 | blanchet | nicer error message from Metis for know failure that isn't the user's fault | changeset | files |
Thu, 14 Apr 2011 11:24:05 +0200 | blanchet | correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)" | changeset | files |
Thu, 14 Apr 2011 11:24:05 +0200 | blanchet | tuning | changeset | files |