Prod is now a parent of Lfp.
Added thm induct2 to Lfp.
Changed the way patterns in abstractions are pretty printed.
It has become simpler now but fails if split has more than one argument
because then the ast-translation does not match.
(* Title: HOL/lfp.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
The Knaster-Tarski Theorem
*)
Lfp = mono + Prod +
consts lfp :: "['a set=>'a set] => 'a set"
defs
(*least fixed point*)
lfp_def "lfp(f) == Inter({u. f(u) <= u})"
end