(* Dies ist nur ein einfacher Kommentar *)

theory Demo = Main:

text {* Dies ist auch ein Kommentar, aus dem man aber auch eine
ansprechenden LaTeX-Präsentation generieren kann! *}

text {*
 Beachten Sie die unterschiedlichen Stile für
 freie Variablen (zB x),
 gebundene Variablen (zB %n)
 und Konstanten (zB Suc).
*}

term "x"
term "Suc x"
term "Succ x"
term "Suc x = Succ y"
prop "Suc y = Suc y"

text{* Typen anzeigen: Menü Isabelle/Isar -> Settings -> Show Types *}

text {* Achtung! 0 und + ist überladen: *}

prop "n + n = 0"
prop "(n::nat) + n = 0"
prop "n + n = Suc m"

text{* Eine gebundene Variable: *}
prop "map (\<lambda>n. Suc n + 1) [0, 1] = [1, 2]";

(*
term "Suc n = True";
Terme muessen typkorrekt sein!
*)

end