# HG changeset patch # User nipkow # Date 1371798026 -7200 # Node ID c2f30ba4bb98b5a8432262be9b9413e54f77adb3 # Parent 56e83c57f95391ae0032e35d9546f7cb7df64979 tuned diff -r 56e83c57f953 -r c2f30ba4bb98 src/HOL/IMP/Denotational.thy --- a/src/HOL/IMP/Denotational.thy Thu Jun 20 17:43:36 2013 +0200 +++ b/src/HOL/IMP/Denotational.thy Fri Jun 21 09:00:26 2013 +0200 @@ -71,10 +71,10 @@ lemma chain_total: "chain S \ S i \ S j \ S j \ S i" by (metis chain_def le_cases lift_Suc_mono_le) -definition cont :: "('a set \ 'a set) \ bool" where +definition cont :: "('a set \ 'b set) \ bool" where "cont f = (\S. chain S \ f(UN n. S n) = (UN n. f(S n)))" -lemma mono_if_cont: fixes f :: "'a set \ 'a set" +lemma mono_if_cont: fixes f :: "'a set \ 'b set" assumes "cont f" shows "mono f" proof fix a b :: "'a set" assume "a \ b"