src/HOLCF/ex/Fix2.thy

hide id, stamps;
added stamp_names_of, name_of;
replaced make_draft by prep_ext;
improved print_sg;
tuned;

(*  Title:      HOLCF/ex/Fix2.thy
    ID:         $Id$
    Author:     Franz Regensburger
    Copyright   1995 Technische Universitaet Muenchen

 Show that fix is the unique least fixed-point operator. 
 From axioms gix1_def,gix2_def it follows that fix = gix

*)

Fix2 = Fix + 

consts

     gix     :: "('a->'a)->'a"

rules

gix1_def "F`(gix`F) = gix`F"
gix2_def "F`y=y ==> gix`F << y"

end