| Fri, 22 Jan 2010 16:56:51 +0100 | haftmann | HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations) | changeset | files |
| Fri, 22 Jan 2010 16:38:58 +0100 | boehmes | merged | changeset | files |
| Fri, 22 Jan 2010 16:38:21 +0100 | boehmes | support skolem constant for extensional arrays in Z3 proofs | changeset | files |