| Wed, 14 Mar 2007 21:40:28 +0100 | huffman | move bounded (bi)linear operator locales from Lim.thy to RealVector.thy | changeset | files |
| Wed, 14 Mar 2007 01:35:02 +0100 | webertj | is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF | changeset | files |
| Tue, 13 Mar 2007 08:49:58 +0100 | urbanc | deleted function for defining candidates and used nominal_primrec instead | changeset | files |
| Mon, 12 Mar 2007 19:23:49 +0100 | wenzelm | syntax: proper body priorty for derived binders; | changeset | files |
| Mon, 12 Mar 2007 19:23:48 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 12 Mar 2007 16:25:39 +0100 | narboux | removes some unused code that used to try to derive a simpler version of the eqvt lemmas | changeset | files |