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/gfp.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Greatest fixed points (requires Lfp too!)
*)
theory Gfp = Lfp:
constdefs
gfp :: "['a set=>'a set] => 'a set"
"gfp(f) == Union({u. u <= f(u)})" (*greatest fixed point*)
end