Quelle  Document.thy

theory Document
  imports Main
begin

section ‹Some section›

subsection ‹Some subsection›

subsection ‹Some subsubsection›

subsubsection ‹Some subsubsubsection›

paragraph ‹A paragraph.›

text ‹Informal bla bla.›

definition "foo = True"  🍋 ‹side remark on 🍋‹foo›\›

definition "bar = False"  🍋 ‹side remark on 🍋‹bar›\›

lemma foo unfolding foo_def ..


paragraph ‹Another paragraph.›

text ‹See also 🍋‹‹\S3› in "isabelle-system"›.›


section ‹Formal proof of Cantor's theorem›

text_raw ‹\isakeeptag{proof}›
text ‹
  Cantor's Theorem states that there is no surjection from
  a set to its powerset. The proof works by diagonalization. E.g.\ see
  🪙 🪙‹http://mathworld.wolfram.com/CantorDiagonalMethod.html›
  🪙 🪙‹https://en.wikipedia.org/wiki/Cantor's_diagonal_argument›
 ›

theorem Cantor: "∄f :: 'a ==> 'a set. ∀A. ∃x. A = f x"
proof
  assume "∃f :: 'a ==> 'a set. ∀A. ∃x. A = f x"
  then obtain 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
  moreover have "a ∈ ?D ⟷ a ∉ f a" by blast
  ultimately show 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.
 ›

end