Wed, 17 Feb 2010 13:48:13 +0100 | haftmann | tuned primrec signature: return definienda | changeset | files |
Wed, 17 Feb 2010 11:21:59 +0100 | haftmann | merged | changeset | files |
Wed, 17 Feb 2010 11:21:47 +0100 | haftmann | example for executable choice | changeset | files |
Wed, 17 Feb 2010 10:43:20 +0100 | haftmann | added simple theory about discrete summation | changeset | files |
Wed, 17 Feb 2010 11:01:01 +0100 | wenzelm | giving up sunbroy2; | changeset | files |
Wed, 17 Feb 2010 09:51:46 +0100 | haftmann | merged | changeset | files |
Wed, 17 Feb 2010 09:48:53 +0100 | haftmann | a draft for an example how to turn specifications involving choice executable | changeset | files |
Wed, 17 Feb 2010 09:48:53 +0100 | haftmann | added lemma map_of_map_restrict; generalized lemma dom_const | changeset | files |