| Mon, 14 Aug 2006 11:13:50 +0200 | chaieb | Reification now handels binders. | changeset | files |
| Wed, 09 Aug 2006 18:41:42 +0200 | paulson | consistent prefixing for skolem functions | changeset | files |
| Wed, 09 Aug 2006 18:39:08 +0200 | paulson | blacklist augmented to block some "unit" theorems that cause unsound resolution proofs | changeset | files |
| Wed, 09 Aug 2006 15:48:51 +0200 | webertj | tuned: string_of_list, string_of_pair | changeset | files |
| Wed, 09 Aug 2006 10:59:58 +0200 | wenzelm | * ProofContext.prems_limit is now -1 by default; | changeset | files |
| Wed, 09 Aug 2006 00:14:28 +0200 | wenzelm | tuned proofs; | changeset | files |
| Wed, 09 Aug 2006 00:12:40 +0200 | wenzelm | global goals/qeds: after_qed operates on Proof.context (potentially local_theory); | changeset | files |