--- a/src/HOL/UNITY/FP.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/UNITY/FP.thy Mon Mar 01 13:40:23 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/UNITY/FP
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
@@ -10,12 +9,10 @@
theory FP imports UNITY begin
-constdefs
-
- FP_Orig :: "'a program => 'a set"
+definition FP_Orig :: "'a program => 'a set" where
"FP_Orig F == Union{A. ALL B. F : stable (A Int B)}"
- FP :: "'a program => 'a set"
+definition FP :: "'a program => 'a set" where
"FP F == {s. F : stable {s}}"
lemma stable_FP_Orig_Int: "F : stable (FP_Orig F Int B)"