| Tue, 07 Jun 2011 23:22:58 +0900 | Cezary Kaliszyk | Testing invariant in Lambda_F_T | changeset | files |
| Tue, 07 Jun 2011 10:40:06 +0100 | Christian Urban | cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file | changeset | files |
| Tue, 07 Jun 2011 08:52:59 +0100 | Christian Urban | fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant | changeset | files |
| Mon, 06 Jun 2011 13:11:04 +0100 | Christian Urban | slightly stronger property in fundef_ex_prop | changeset | files |
| Sun, 05 Jun 2011 21:14:23 +0100 | Christian Urban | added an option for an invariant (at the moment only a stub) | changeset | files |
| Sun, 05 Jun 2011 16:58:18 +0100 | Christian Urban | added a more general lemma fro fundef_ex1 | changeset | files |
| Sat, 04 Jun 2011 14:50:57 +0900 | Cezary Kaliszyk | Trying the induction on the graph | changeset | files |