| 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 |
| Thu, 14 Apr 2011 11:24:05 +0200 | blanchet | remove needless export | changeset | files |
| Thu, 14 Apr 2011 11:24:05 +0200 | blanchet | more clausification tests | changeset | files |
| Thu, 14 Apr 2011 11:24:05 +0200 | blanchet | make 48170228f562 work also with "HO_Reas" examples | changeset | files |