| Thu, 08 Dec 2005 20:15:50 +0100 | wenzelm | tuned proofs; | changeset | files |
| Thu, 08 Dec 2005 20:15:41 +0100 | wenzelm | Cla.swap; | changeset | files |
| Thu, 08 Dec 2005 20:15:34 +0100 | wenzelm | removed hint for Classical.swap, which is not really user-level anyway; | changeset | files |
| Thu, 08 Dec 2005 12:50:04 +0100 | wenzelm | tuned sources and proofs | changeset | files |
| Thu, 08 Dec 2005 12:50:03 +0100 | wenzelm | Classical.swap; | changeset | files |
| Thu, 08 Dec 2005 12:50:02 +0100 | wenzelm | * HOL: Theorem 'swap' is no longer bound at the ML top-level. | changeset | files |
| Thu, 08 Dec 2005 10:17:21 +0100 | berghofe | Adapted to new type of PureThy.add_defs_i. | changeset | files |
| Wed, 07 Dec 2005 16:47:04 +0100 | wenzelm | replaced swap by Classical.swap; | changeset | files |
| Wed, 07 Dec 2005 15:23:22 +0100 | wenzelm | avoid unportable tail; | changeset | files |
| Wed, 07 Dec 2005 12:33:38 +0100 | urbanc | tuned | changeset | files |
| Tue, 06 Dec 2005 17:26:26 +0100 | haftmann | removed thms 'swap' and 'nth_map' from ML toplevel | changeset | files |
| Tue, 06 Dec 2005 17:11:40 +0100 | haftmann | improved serialization of classes to haskell | changeset | files |
| Tue, 06 Dec 2005 16:07:25 +0100 | haftmann | improved class handling | changeset | files |
| Tue, 06 Dec 2005 16:07:10 +0100 | haftmann | added 'dig' combinator | changeset | files |
| Tue, 06 Dec 2005 09:04:09 +0100 | haftmann | re-oriented some result tuples in PureThy | changeset | files |
| Tue, 06 Dec 2005 06:22:14 +0100 | mengj | Added more functions for new type embedding of HOL clauses. | changeset | files |
| Tue, 06 Dec 2005 06:21:07 +0100 | mengj | Added new type embedding methods for translating HOL clauses. | changeset | files |
| Mon, 05 Dec 2005 18:19:49 +0100 | urbanc | added code to say that discrete types (nat, bool, char) | changeset | files |
| Mon, 05 Dec 2005 17:02:20 +0100 | urbanc | tuned | changeset | files |
| Mon, 05 Dec 2005 15:55:19 +0100 | urbanc | transitivity should be now in a reasonable state. But | changeset | files |
| Mon, 05 Dec 2005 10:33:30 +0100 | urbanc | tuned | changeset | files |
| Mon, 05 Dec 2005 10:32:37 +0100 | urbanc | ISAR-fied two proofs | changeset | files |
| Mon, 05 Dec 2005 00:39:18 +0100 | berghofe | Adapted to new type of store_thmss(_atts). | changeset | files |
| Mon, 05 Dec 2005 00:38:07 +0100 | berghofe | Added store_thmss_atts to signature again. | changeset | files |
| Sun, 04 Dec 2005 12:40:39 +0100 | urbanc | tuned | changeset | files |
| Sun, 04 Dec 2005 12:25:57 +0100 | urbanc | tuned | changeset | files |
| Sun, 04 Dec 2005 12:14:40 +0100 | urbanc | tuned | changeset | files |
| Sun, 04 Dec 2005 12:14:27 +0100 | urbanc | added an Isar-proof for the abs_ALL lemma | changeset | files |
| Sun, 04 Dec 2005 12:14:03 +0100 | urbanc | tuning | changeset | files |
| Fri, 02 Dec 2005 22:57:36 +0100 | wenzelm | defines: beta/eta contract lhs; | changeset | files |