src/HOL/Wellfounded_Relations.thy
changeset 11136 e34e7f6d9b57
parent 11008 f7333f055ef6
child 11451 8abfb4f7bd02
     1.1 --- a/src/HOL/Wellfounded_Relations.thy	Thu Feb 15 16:00:38 2001 +0100
     1.2 +++ b/src/HOL/Wellfounded_Relations.thy	Thu Feb 15 16:00:40 2001 +0100
     1.3 @@ -21,9 +21,6 @@
     1.4   less_than :: "(nat*nat)set"
     1.5  "less_than == trancl pred_nat"
     1.6  
     1.7 - inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
     1.8 -"inv_image r f == {(x,y). (f(x), f(y)) : r}"
     1.9 -
    1.10   measure   :: "('a => nat) => ('a * 'a)set"
    1.11  "measure == inv_image less_than"
    1.12