added some lemmas to the collection "abs_fresh"
the lemmas are of the form
finite (supp x) ==> (b # [a].x) = (b=a \/ b # x)
previously only lemmas of the form
(b # [a].x) = (b=a \/ b # x)
with the type-constraint that x is finitely supported
were included.
(* Title: CCL/Gfp.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
header {* Greatest fixed points *}
theory Gfp
imports Lfp
begin
constdefs
gfp :: "['a set=>'a set] => 'a set" (*greatest fixed point*)
"gfp(f) == Union({u. u <= f(u)})"
ML {* use_legacy_bindings (the_context ()) *}
end