src/Doc/Demo_FoilTeX/Document.thy

typo

theory Document
  imports Main
begin

section \<open>Abstract\<close>

text \<open>
  \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
  \<^url>\<open>https://ctan.org/pkg/foiltex\<close> for further information.
\<close>


chapter \<open>Introduction\<close>

section \<open>Some slide\<close>

paragraph \<open>Point 1:
  \plainstyle ABC\<close>

text \<open>
  \<^item> something
  \<^item> to say \dots
\<close>

paragraph \<open>Point 2:
  \plainstyle XYZ\<close>

text \<open>
  \<^item> more
  \<^item> to say \dots
\<close>


section \<open>Another slide\<close>

paragraph \<open>Key definitions:\<close>

text \<open>Informal bla bla.\<close>

definition "foo = True"  \<comment> \<open>side remark on \<^const>\<open>foo\<close>\<close>

definition "bar = False"  \<comment> \<open>side remark on \<^const>\<open>bar\<close>\<close>

lemma foo unfolding foo_def ..


chapter \<open>Application: Cantor's theorem\<close>

section \<open>Informal notes\<close>

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

section \<open>Formal proof\<close>

theorem Cantor: "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
proof
  assume "\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
  then obtain f :: "'a \<Rightarrow> 'a set" where *: "\<forall>A. \<exists>x. A = f x" ..
  let ?D = "{x. x \<notin> f x}"
  from * obtain a where "?D = f a" by blast
  moreover have "a \<in> ?D \<longleftrightarrow> a \<notin> f a" by blast
  ultimately show False by blast
qed


chapter \<open>Conclusion\<close>

section \<open>Lorem ipsum dolor\<close>

text \<open>
  \<^item> Lorem ipsum dolor sit amet, consectetur adipiscing elit.
  \<^item> Donec id ipsum sapien.
  \<^item> Vivamus malesuada enim nibh, a tristique nisi sodales ac.
  \<^item> Praesent ut sem consectetur, interdum tellus ac, sodales nulla.
\<close>

end