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 |