| Thu, 15 Jul 1999 17:53:28 +0200 | wenzelm | export init_state; | changeset | files |
| Thu, 15 Jul 1999 10:34:37 +0200 | paulson | more renaming of theorems from _nat to _int (corresponding to a function that | changeset | files |
| Thu, 15 Jul 1999 10:34:00 +0200 | paulson | more renaming of theorems from _nat to _int (corresponding to a function that | changeset | files |
| Thu, 15 Jul 1999 10:33:16 +0200 | paulson | qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int | changeset | files |
| Thu, 15 Jul 1999 10:27:54 +0200 | paulson | qed_goal -> Goal | changeset | files |
| Wed, 14 Jul 1999 13:32:21 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 14 Jul 1999 13:07:09 +0200 | wenzelm | tuned comments; | changeset | files |
| Wed, 14 Jul 1999 13:06:08 +0200 | wenzelm | tuned contradiction method; | changeset | files |
| Wed, 14 Jul 1999 13:05:46 +0200 | wenzelm | improved comment; | changeset | files |
| Wed, 14 Jul 1999 13:05:28 +0200 | wenzelm | more marg_comments; | changeset | files |
| Wed, 14 Jul 1999 12:28:12 +0200 | wenzelm | Deriving rules in Isabelle; | changeset | files |
| Wed, 14 Jul 1999 10:41:33 +0200 | paulson | rewrite add1_zle_eq is no longer in the default simpset | changeset | files |
| Wed, 14 Jul 1999 10:40:51 +0200 | paulson | optimization for division by powers of 2 | changeset | files |
| Wed, 14 Jul 1999 10:40:11 +0200 | paulson | new montonicity theorems | changeset | files |
| Wed, 14 Jul 1999 10:39:26 +0200 | paulson | new constant folding rewrites | changeset | files |
| Tue, 13 Jul 1999 13:54:08 +0200 | wenzelm | handle cgoal; | changeset | files |
| Tue, 13 Jul 1999 13:53:34 +0200 | wenzelm | added mk_cgoal, assume_goal; | changeset | files |
| Tue, 13 Jul 1999 12:32:22 +0200 | wenzelm | same_tac; | changeset | files |
| Tue, 13 Jul 1999 10:45:47 +0200 | paulson | change to force (m div 0 = 0) | changeset | files |
| Tue, 13 Jul 1999 10:45:09 +0200 | paulson | many new theorems | changeset | files |
| Tue, 13 Jul 1999 10:44:45 +0200 | paulson | renamed inj_nat to inj_int | changeset | files |
| Tue, 13 Jul 1999 10:44:13 +0200 | paulson | new monotonicity theorems | changeset | files |
| Tue, 13 Jul 1999 10:43:31 +0200 | paulson | new theorem zmult_eq_0_iff | changeset | files |
| Tue, 13 Jul 1999 10:42:31 +0200 | paulson | renamed sort "numeral" to "number" | changeset | files |
| Tue, 13 Jul 1999 10:41:59 +0200 | paulson | simplified the <= monotonicity proof | changeset | files |
| Mon, 12 Jul 1999 22:29:38 +0200 | wenzelm | local qeds: print rule; | changeset | files |
| Mon, 12 Jul 1999 22:29:17 +0200 | wenzelm | added show_hyps flag; | changeset | files |
| Mon, 12 Jul 1999 22:28:56 +0200 | wenzelm | local qed; print rule; | changeset | files |
| Mon, 12 Jul 1999 22:28:38 +0200 | wenzelm | term/prop: include number; | changeset | files |
| Mon, 12 Jul 1999 22:27:51 +0200 | wenzelm | added show_hyps flag; | changeset | files |
| Mon, 12 Jul 1999 22:27:20 +0200 | wenzelm | export assumption_tac; | changeset | files |
| Mon, 12 Jul 1999 22:25:39 +0200 | wenzelm | removed merge_theories; | changeset | files |