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
|