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
|
Tue, 07 Sep 1999 18:10:03 +0200 |
wenzelm |
\indexisarmeth: "Methods";
|
changeset |
files
|
Tue, 07 Sep 1999 18:09:40 +0200 |
wenzelm |
tuned (then_)apply;
|
changeset |
files
|
Tue, 07 Sep 1999 18:09:18 +0200 |
wenzelm |
url;
|
changeset |
files
|
Tue, 07 Sep 1999 18:09:04 +0200 |
wenzelm |
\url;
|
changeset |
files
|
Tue, 07 Sep 1999 18:08:51 +0200 |
wenzelm |
induct method: rule option;
|
changeset |
files
|
Tue, 07 Sep 1999 17:21:44 +0200 |
wenzelm |
Method.refine_no_facts;
|
changeset |
files
|
Tue, 07 Sep 1999 16:57:52 +0200 |
wenzelm |
read_def_termT: dummyT;
|
changeset |
files
|
Tue, 07 Sep 1999 16:57:28 +0200 |
wenzelm |
then_tac = refine;
|
changeset |
files
|
Tue, 07 Sep 1999 16:57:15 +0200 |
wenzelm |
read_typ/term: context_of;
|
changeset |
files
|
Tue, 07 Sep 1999 16:56:47 +0200 |
wenzelm |
tuned;
|
changeset |
files
|