theorem Cantor: "∄f :: 'a → 'a set. ∀A. ∃x. A = f x" proof assume"∃f :: 'a → 'a set. ∀A. ∃x. A = f x" thenobtain f :: "'a → 'a set"where *: "∀A. ∃x. A = f x" .. let ?D = "{x. x ∉ f x}" from * obtain a where"?D = f a"by blast moreoverhave"a ∈ ?D ⟷ a ∉ f a"by blast ultimatelyshow False by blast qed
subsection‹Lorem ipsum dolor›
text‹
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Donec id ipsum
sapien. Vivamus malesuada enim nibh, a tristique nisi sodales ac. Praesent
ut sem consectetur, interdum tellus ac, sodales nulla. Quisque vel diam at
risus tempus tempor eget a tortor. Suspendisse potenti. Nulla erat lacus,
dignissim sed volutpat nec, feugiat non leo. Nunc blandit et justo sed
venenatis. Donec scelerisque placerat magna, et congue nulla convallis vel.
Cras tristique dolor consequat dolor tristique rutrum. Suspendisse ultrices
sem nibh, et suscipit felis ultricies at. Aliquam venenatis est vel nulla
efficitur ornare. Lorem ipsum dolor sit amet, consectetur adipiscing elit. ›
text_raw‹\begin{credits}›
subsubsection‹\ackname› text‹
Isabelle/Scala was of great help to assemble the ▩‹llncs› system component;
see also 🚫‹~~/src/Pure/Admin/component_llncs.scala› and 🚫‹$ISABELLE_LLNCS_HOME›. ›
subsubsection‹\discintname› text‹
I have a long-standing interest in the wealth and prosperity of the Isabelle
open-source project. ›
text_raw‹\end{credits}›
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet am 2026-09-28)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
