src/HOL/Wellfounded_Relations.thy
changeset 11454 7514e5e21cb8
parent 11451 8abfb4f7bd02
child 12398 9c27f28c8f5a
     1.1 --- a/src/HOL/Wellfounded_Relations.thy	Wed Jul 25 13:44:32 2001 +0200
     1.2 +++ b/src/HOL/Wellfounded_Relations.thy	Wed Jul 25 17:58:26 2001 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  separately.
     1.5  *)
     1.6  
     1.7 -Wellfounded_Relations = Finite + Hilbert_Choice + 
     1.8 +Wellfounded_Relations = Finite + 
     1.9  
    1.10  (* logically belongs in Finite.thy, but the theorems are proved in Finite.ML *)
    1.11  instance unit :: finite                  (finite_unit)