| 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 |
| Wed, 26 May 2004 11:43:50 +0200 | paulson | more group isomorphisms | changeset | files |