changeset 13894 | 8018173a7979 |
parent 13893 | 19849d258890 |
child 13895 | b6105462ccd3 |
--- a/src/CCL/gfp.thy Sat Apr 05 16:00:00 2003 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* Title: HOL/gfp.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Greatest fixed points -*) - -Gfp = Lfp + -consts gfp :: "['a set=>'a set] => 'a set" -rules - (*greatest fixed point*) - gfp_def "gfp(f) == Union({u. u <= f(u)})" -end