renamed Finite to Finite_Set;
authorwenzelm
Thu Dec 06 00:40:04 2001 +0100 (2001-12-06)
changeset 123989c27f28c8f5a
parent 12397 6766aa05e4eb
child 12399 2ba27248af7f
renamed Finite to Finite_Set;
src/HOL/Integ/Equiv.thy
src/HOL/Wellfounded_Relations.thy
     1.1 --- a/src/HOL/Integ/Equiv.thy	Thu Dec 06 00:39:40 2001 +0100
     1.2 +++ b/src/HOL/Integ/Equiv.thy	Thu Dec 06 00:40:04 2001 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Equivalence relations in Higher-Order Set Theory 
     1.5  *)
     1.6  
     1.7 -Equiv = Relation + Finite + 
     1.8 +Equiv = Relation + Finite_Set +
     1.9  constdefs
    1.10    equiv    :: "['a set, ('a*'a) set] => bool"
    1.11      "equiv A r == refl A r & sym(r) & trans(r)"
     2.1 --- a/src/HOL/Wellfounded_Relations.thy	Thu Dec 06 00:39:40 2001 +0100
     2.2 +++ b/src/HOL/Wellfounded_Relations.thy	Thu Dec 06 00:40:04 2001 +0100
     2.3 @@ -10,12 +10,7 @@
     2.4  separately.
     2.5  *)
     2.6  
     2.7 -Wellfounded_Relations = Finite + 
     2.8 -
     2.9 -(* logically belongs in Finite.thy, but the theorems are proved in Finite.ML *)
    2.10 -instance unit :: finite                  (finite_unit)
    2.11 -instance "*" :: (finite,finite) finite   (finite_Prod)
    2.12 -
    2.13 +Wellfounded_Relations = Finite_Set + 
    2.14  
    2.15  constdefs
    2.16   less_than :: "(nat*nat)set"