| Fri, 16 Feb 2001 00:36:21 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 15 Feb 2001 17:18:54 +0100 |
wenzelm |
eliminate get_def;
Isabelle99-2
|
changeset |
files
|
| Thu, 15 Feb 2001 16:12:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 15 Feb 2001 16:07:57 +0100 |
oheimb |
Ord.thy/.ML converted to Isar
|
changeset |
files
|
| Thu, 15 Feb 2001 16:01:47 +0100 |
oheimb |
moved inv_image to Relation
|
changeset |
files
|
| Thu, 15 Feb 2001 16:01:34 +0100 |
oheimb |
supressed some warnings on identical proofstate
|
changeset |
files
|
| Thu, 15 Feb 2001 16:01:22 +0100 |
oheimb |
Ord.thy/.ML converted to Isar
|
changeset |
files
|
| Thu, 15 Feb 2001 16:01:07 +0100 |
oheimb |
moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least
|
changeset |
files
|
| Thu, 15 Feb 2001 16:00:44 +0100 |
oheimb |
simplified proof of Least_mono
|
changeset |
files
|
| Thu, 15 Feb 2001 16:00:42 +0100 |
oheimb |
added wellorder axclass
|
changeset |
files
|
| Thu, 15 Feb 2001 16:00:40 +0100 |
oheimb |
moved inv_image to Relation
|
changeset |
files
|
| Thu, 15 Feb 2001 16:00:38 +0100 |
oheimb |
moved wf_less from Nat.ML to NatDef.ML
|
changeset |
files
|
| Thu, 15 Feb 2001 16:00:36 +0100 |
oheimb |
added nat as instance of new wellorder axclass
|
changeset |
files
|
| Thu, 15 Feb 2001 16:00:35 +0100 |
oheimb |
Ord.thy/.ML converted to Isar
|
changeset |
files
|
| Thu, 15 Feb 2001 15:56:51 +0100 |
oheimb |
added trial proof
|
changeset |
files
|
| Thu, 15 Feb 2001 14:30:13 +0100 |
oheimb |
improved subst_RS
|
changeset |
files
|