| Wed, 08 Sep 1999 23:49:39 +0200 |
wenzelm |
lemma less_add;
|
changeset |
files
|
| Wed, 08 Sep 1999 18:10:39 +0200 |
wenzelm |
(un)fold: ignore facts;
|
changeset |
files
|
| Wed, 08 Sep 1999 16:44:11 +0200 |
paulson |
more rational theorem names (?)
|
changeset |
files
|
| Wed, 08 Sep 1999 16:43:26 +0200 |
paulson |
tidied
|
changeset |
files
|
| Wed, 08 Sep 1999 15:50:11 +0200 |
paulson |
more rational theorem names (?)
|
changeset |
files
|
| Wed, 08 Sep 1999 15:45:36 +0200 |
paulson |
ensures_tac now handles leadsTo as well as LeadsTo
|
changeset |
files
|
| Wed, 08 Sep 1999 15:44:56 +0200 |
paulson |
new theorem single_Diff_lessThan
|
changeset |
files
|
| Wed, 08 Sep 1999 15:44:11 +0200 |
paulson |
now uses the identity function
|
changeset |
files
|
| Wed, 08 Sep 1999 15:41:58 +0200 |
paulson |
simplification of relations involving 0, Suc and natural-number numerals
|
changeset |
files
|
| Wed, 08 Sep 1999 15:41:30 +0200 |
paulson |
generalized the theorem zless_zero_nat to zless_nat_eq_int_zless, and
|
changeset |
files
|
| Wed, 08 Sep 1999 15:40:39 +0200 |
paulson |
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
|
changeset |
files
|
| Wed, 08 Sep 1999 15:39:52 +0200 |
paulson |
moved identity theorems to Fun.ML
|
changeset |
files
|
| Wed, 08 Sep 1999 15:38:54 +0200 |
paulson |
comments
|
changeset |
files
|
| Wed, 08 Sep 1999 15:38:12 +0200 |
paulson |
images and preimages of the identity function
|
changeset |
files
|
| Wed, 08 Sep 1999 15:37:31 +0200 |
paulson |
new example HOL/UNITY/TimerArray
|
changeset |
files
|
| Tue, 07 Sep 1999 18:10:33 +0200 |
wenzelm |
rule option;
|
changeset |
files
|