Records:
- Record types are now by default printed with their type abbreviation
instead of the list of all field types. This can be configured via
the reference "print_record_type_abbr".
- Simproc "record_upd_simproc" for simplification of multiple updates
added (not enabled by default).
- Tactic "record_split_simp_tac" to split and simplify records added.
- Bug-fix and optimisation of "record_simproc".
- "record_simproc" and "record_upd_simproc" are now sensitive to
quick_and_dirty flag.
(* Title: HOL/Lfp.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
The Knaster-Tarski Theorem
*)
theory Lfp = Product_Type:
constdefs
lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"
"lfp(f) == Inter({u. f(u) <= u})" (*least fixed point*)
end