src/HOL/Wellfounded_Relations.thy
changeset 12398 9c27f28c8f5a
parent 11454 7514e5e21cb8
child 15346 ac272926fb77
     1.1 --- a/src/HOL/Wellfounded_Relations.thy	Thu Dec 06 00:39:40 2001 +0100
     1.2 +++ b/src/HOL/Wellfounded_Relations.thy	Thu Dec 06 00:40:04 2001 +0100
     1.3 @@ -10,12 +10,7 @@
     1.4  separately.
     1.5  *)
     1.6  
     1.7 -Wellfounded_Relations = Finite + 
     1.8 -
     1.9 -(* logically belongs in Finite.thy, but the theorems are proved in Finite.ML *)
    1.10 -instance unit :: finite                  (finite_unit)
    1.11 -instance "*" :: (finite,finite) finite   (finite_Prod)
    1.12 -
    1.13 +Wellfounded_Relations = Finite_Set + 
    1.14  
    1.15  constdefs
    1.16   less_than :: "(nat*nat)set"