| Fri, 12 Mar 2010 18:43:22 +0100 | nipkow | merged | changeset | files |
| Fri, 12 Mar 2010 18:42:56 +0100 | nipkow | Reorganized Hoare logic theories; added Hoare_Den | changeset | files |
| Fri, 12 Mar 2010 16:02:42 +0100 | hoelzl | merged | changeset | files |
| Tue, 09 Mar 2010 15:42:23 +0100 | himmelma | reset smt_certificates | changeset | files |
| Tue, 09 Mar 2010 15:39:26 +0100 | himmelma | added lemmas | changeset | files |
| Fri, 12 Mar 2010 15:48:37 +0100 | nipkow | merged | changeset | files |
| Fri, 12 Mar 2010 15:48:18 +0100 | nipkow | Added Hoare_Op.thy | changeset | files |
| Fri, 12 Mar 2010 15:35:41 +0100 | hoelzl | Equality of integral and infinite sum. | changeset | files |
| Fri, 12 Mar 2010 12:02:22 +0100 | blanchet | make tests less demanding, to prevent sporadic failures | changeset | files |
| Sat, 13 Mar 2010 15:12:56 +0100 | wenzelm | more antiquotations; | changeset | files |
| Sat, 13 Mar 2010 15:12:47 +0100 | wenzelm | command 'typedef' now works within a local theory context; | changeset | files |
| Sat, 13 Mar 2010 15:12:17 +0100 | wenzelm | removed obsolete HOL 'typedecl'; | changeset | files |
| Sat, 13 Mar 2010 14:44:47 +0100 | wenzelm | adapted to localized typedef: handle single global interpretation only; | changeset | files |
| Sat, 13 Mar 2010 14:43:04 +0100 | wenzelm | global typedef; | changeset | files |