Thu, 02 Feb 2012 12:42:05 +0100 | blanchet | don't introduce new symbols in helpers -- makes problems unprovable | changeset | files |
Thu, 02 Feb 2012 12:42:05 +0100 | blanchet | only constants can be aliased | changeset | files |
Thu, 02 Feb 2012 12:42:05 +0100 | blanchet | include new SPASS by default if available | changeset | files |
Thu, 02 Feb 2012 10:16:10 +0100 | bulwahn | adding an example for finite and cofinite sets | changeset | files |
Thu, 02 Feb 2012 10:12:30 +0100 | bulwahn | adding a minimally refined equality on sets for code generation | changeset | files |
Thu, 02 Feb 2012 10:12:11 +0100 | bulwahn | adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type | changeset | files |