| Wed, 26 May 2004 19:06:09 +0200 | chaieb | abstraction over functions is no default any more. | changeset | files |
| Wed, 26 May 2004 18:52:18 +0200 | webertj | adjusted for different signature of Type.typ_instance | changeset | files |
| Wed, 26 May 2004 18:23:46 +0200 | webertj | mainly new/different datatype examples | changeset | files |
| Wed, 26 May 2004 18:06:38 +0200 | webertj | documentation updated | changeset | files |
| Wed, 26 May 2004 18:03:52 +0200 | webertj | major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them) | changeset | files |
| Wed, 26 May 2004 17:43:52 +0200 | webertj | new default parameters for refute | changeset | files |
| Wed, 26 May 2004 17:42:46 +0200 | webertj | solver "auto" now issues a warning when it uses solver "enumerate" | changeset | files |
| Wed, 26 May 2004 14:57:06 +0200 | nipkow | Corrected printer bug for bounded quantifiers Q x<=y. P | changeset | files |