| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Demo_FoilTeX/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 2 kB |
|
Quelle Document.thy Sprache: Isabelle |
|||||||||
|
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: "\ proof assume "\ then obtain f :: "'a \ let ?D = "{x. x \ from * obtain a where "?D = f a" by blast moreover have "a \ 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 ¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28