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 |
Fri, 22 Jan 2010 16:33:44 +0100 | boehmes | drop underscores at end of names coming from Boogie | changeset | files |
Fri, 22 Jan 2010 15:26:29 +0100 | bulwahn | merged | changeset | files |
Fri, 22 Jan 2010 11:42:28 +0100 | bulwahn | correctly hiding facts of Lazy_Sequence | changeset | files |
Thu, 21 Jan 2010 14:13:21 +0100 | bulwahn | corrected and simplified Spec_Rules registration in the Recdef package | changeset | files |