Thu, 02 Jan 2014 09:50:22 +0100 | blanchet | gracefully handle single-equation case, where 'nchotomy' is 'True' | changeset | files |
Thu, 02 Jan 2014 09:50:22 +0100 | blanchet | made tactic handle gracefully the case of missing constructors | changeset | files |
Thu, 02 Jan 2014 09:50:22 +0100 | blanchet | removed 'nchotomy' property | changeset | files |
Thu, 02 Jan 2014 09:50:22 +0100 | blanchet | don't generate any proof obligation for implicit (de facto) exclusiveness | changeset | files |
Thu, 02 Jan 2014 09:50:22 +0100 | blanchet | detect syntactic exhaustiveness | changeset | files |
Thu, 02 Jan 2014 09:50:22 +0100 | blanchet | internally allow different values for 'exhaustive' for different constructors | changeset | files |