| Tue, 24 Mar 2009 12:45:23 +0100 | nipkow | merged | changeset | files |
| Tue, 24 Mar 2009 12:45:01 +0100 | nipkow | presburger uses [arith] now | changeset | files |
| Tue, 24 Mar 2009 12:01:12 +0100 | wenzelm | merged | changeset | files |
| Tue, 24 Mar 2009 09:15:59 +0100 | haftmann | merged | changeset | files |
| Tue, 24 Mar 2009 09:15:51 +0100 | haftmann | added Imperative_HOL_ex | changeset | files |
| Tue, 24 Mar 2009 15:55:11 +1100 | Timothy Bourke | Use assms rather than prems in find_theorems solves. | changeset | files |
| Mon, 23 Mar 2009 14:29:59 -0700 | huffman | clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros | changeset | files |
| Mon, 23 Mar 2009 13:26:52 -0700 | huffman | lemmas add_sign_intros | changeset | files |
| Mon, 23 Mar 2009 19:01:34 +0100 | haftmann | merged | changeset | files |
| Mon, 23 Mar 2009 19:01:17 +0100 | haftmann | moved Imperative_HOL examples to Imperative_HOL/ex | changeset | files |
| Mon, 23 Mar 2009 19:01:17 +0100 | haftmann | corrected variable renaming | changeset | files |
| Mon, 23 Mar 2009 19:01:16 +0100 | haftmann | tuned error messages | changeset | files |