author | oheimb |
Thu, 27 Jun 1996 12:53:08 +0200 | |
changeset 1832 | 79dd1433867c |
parent 1479 | 21eb5e156d91 |
child 2570 | 24d7e8fb8261 |
permissions | -rw-r--r-- |
(* 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