src/HOL/Wellfounded_Relations.thy
changeset 11451 8abfb4f7bd02
parent 11136 e34e7f6d9b57
child 11454 7514e5e21cb8
     1.1 --- a/src/HOL/Wellfounded_Relations.thy	Tue Jul 24 11:25:54 2001 +0200
     1.2 +++ b/src/HOL/Wellfounded_Relations.thy	Wed Jul 25 13:13:01 2001 +0200
     1.3 @@ -10,9 +10,9 @@
     1.4  separately.
     1.5  *)
     1.6  
     1.7 -Wellfounded_Relations = Finite +
     1.8 +Wellfounded_Relations = Finite + Hilbert_Choice + 
     1.9  
    1.10 -(* actually belongs to theory Finite *)
    1.11 +(* logically belongs in Finite.thy, but the theorems are proved in Finite.ML *)
    1.12  instance unit :: finite                  (finite_unit)
    1.13  instance "*" :: (finite,finite) finite   (finite_Prod)
    1.14