Impressum Document.thy   Sprache: Isabelle

theory Document
  imports Main
begin

section ‹Abstract›

text ‹
  \small
  Isabelle is a formal document preparation system. This example shows how to
  use it together with Foil{\TeX} to produce slides in {\LaTeX}. See
  🚫‹https://ctan.org/pkg/foiltex› for further information.
›


chapter ‹Introduction›

section ‹Some slide›

paragraph ‹Point 1:
  \plainstyle ABC›

text ‹
  🚫 something
  🚫 to say \dots
›

paragraph ‹Point 2:
  \plainstyle XYZ›

text ‹
  🚫 more
  🚫 to say \dots
›


section ‹Another slide›

paragraph ‹Key definitions:›

text ‹Informal bla bla.›

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

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

lemma foo unfolding foo_def ..


chapter ‹Application: Cantor's theorem\

section ‹Informal notes›

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\
›

section ‹Formal proof›

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


chapter ‹Conclusion›

section ‹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.
›

end