diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Conditionally_Complete_Lattices.thy --- a/src/HOL/Conditionally_Complete_Lattices.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Sun Nov 26 21:08:32 2017 +0100 @@ -430,7 +430,7 @@ assumes "a < b" and "P a" and "\ P b" shows "\c. a \ c \ c \ b \ (\x. a \ x \ x < c \ P x) \ (\d. (\x. a \ x \ x < d \ P x) \ d \ c)" -proof (rule exI [where x = "Sup {d. \x. a \ x & x < d --> P x}"], auto) +proof (rule exI [where x = "Sup {d. \x. a \ x \ x < d \ P x}"], auto) show "a \ Sup {d. \c. a \ c \ c < d \ P c}" by (rule cSup_upper, auto simp: bdd_above_def) (metis \a < b\ \\ P b\ linear less_le) @@ -439,7 +439,7 @@ apply (rule cSup_least) apply auto apply (metis less_le_not_le) - apply (metis \a \~ P b\ linear less_le) + apply (metis \a \\ P b\ linear less_le) done next fix x @@ -454,7 +454,7 @@ assume 0: "\x. a \ x \ x < d \ P x" thus "d \ Sup {d. \c. a \ c \ c < d \ P c}" by (rule_tac cSup_upper, auto simp: bdd_above_def) - (metis \a \~ P b\ linear less_le) + (metis \a \\ P b\ linear less_le) qed end