diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/BNF_Greatest_Fixpoint.thy --- a/src/HOL/BNF_Greatest_Fixpoint.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy Sun Nov 26 21:08:32 2017 +0100 @@ -36,7 +36,7 @@ lemma equiv_proj: assumes e: "equiv A R" and m: "z \ R" - shows "(proj R o fst) z = (proj R o snd) z" + shows "(proj R \ fst) z = (proj R \ snd) z" proof - from m have z: "(fst z, snd z) \ R" by auto with e have "\x. (fst z, x) \ R \ (snd z, x) \ R" "\x. (snd z, x) \ R \ (fst z, x) \ R" @@ -139,10 +139,10 @@ lemma fst_diag_id: "(fst \ (\x. (x, x))) z = id z" by simp lemma snd_diag_id: "(snd \ (\x. (x, x))) z = id z" by simp -lemma fst_diag_fst: "fst o ((\x. (x, x)) o fst) = fst" by auto -lemma snd_diag_fst: "snd o ((\x. (x, x)) o fst) = fst" by auto -lemma fst_diag_snd: "fst o ((\x. (x, x)) o snd) = snd" by auto -lemma snd_diag_snd: "snd o ((\x. (x, x)) o snd) = snd" by auto +lemma fst_diag_fst: "fst \ ((\x. (x, x)) \ fst) = fst" by auto +lemma snd_diag_fst: "snd \ ((\x. (x, x)) \ fst) = fst" by auto +lemma fst_diag_snd: "fst \ ((\x. (x, x)) \ snd) = snd" by auto +lemma snd_diag_snd: "snd \ ((\x. (x, x)) \ snd) = snd" by auto definition Succ where "Succ Kl kl = {k . kl @ [k] \ Kl}" definition Shift where "Shift Kl k = {kl. k # kl \ Kl}"