Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma

Benutzer


products/Sources/formale Sprachen/Isabelle/Doc/Demo_FoilTeX/ (Isabelle Prover Version 2025-1^©) Datei vom 16.11.2025 mit Größe 2 kB

Quelle 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 const‹foo››

definition "bar = False"  ― ‹side remark on const‹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

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-06-29) ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Haftungshinweis

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.