Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Core_Nits.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Nitpick_Examples/Core_Nits.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2009-2011

Examples featuring Nitpick's functional core.
*)

section \<open>Examples Featuring Nitpick's Functional Core\<close>

theory Core_Nits
imports Main
begin

nitpick_params [verbose, card = 1-6, unary_ints, max_potential = 0,
                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]

subsection \<open>Curry in a Hurry\<close>

lemma "(\f x y. (curry o case_prod) f x y) = (\f x y. (\x. x) f x y)"
nitpick [card = 1-12, expect = none]
by auto

lemma "(\f p. (case_prod o curry) f p) = (\f p. (\x. x) f p)"
nitpick [card = 1-12, expect = none]
by auto

lemma "case_prod (curry f) = f"
nitpick [card = 1-12, expect = none]
by auto

lemma "curry (case_prod f) = f"
nitpick [card = 1-12, expect = none]
by auto

lemma "case_prod (\x y. f (x, y)) = f"
nitpick [card = 1-12, expect = none]
by auto

subsection \<open>Representations\<close>

lemma "\f. f = (\x. x) \ f y = y"
nitpick [expect = none]
by auto

lemma "(\g. \x. g (f x) = x) \ (\y. \x. y = f x)"
nitpick [card 'a = 25, card 'b = 24, expect = genuine]
nitpick [card = 1-10, mono, expect = none]
oops

lemma "\f. f = (\x. x) \ f y \ y"
nitpick [card = 1, expect = genuine]
oops

lemma "P (\x. x)"
nitpick [card = 1, expect = genuine]
oops

lemma "{(a::'a\'a, b::'b)}\ = {(b, a)}"
nitpick [card = 1-12, expect = none]
by auto

lemma "fst (a, b) = a"
nitpick [card = 1-20, expect = none]
by auto

lemma "\P. P = Id"
nitpick [card = 1-20, expect = none]
by auto

lemma "(a::'a\'b, a) \ Id\<^sup>*"
nitpick [card = 1-2, expect = none]
by auto

lemma "(a::'a\'a, a) \ Id\<^sup>* \ {(a, b)}\<^sup>*"
nitpick [card = 1-4, expect = none]
by auto

lemma "(a, a) \ Id"
nitpick [card = 1-50, expect = none]
by (auto simp: Id_def)

lemma "((a::'a, b::'a), (a, b)) \ Id"
nitpick [card = 1-10, expect = none]
by (auto simp: Id_def)

lemma "(x::'a\'a) \ UNIV"
nitpick [card = 1-50, expect = none]
sorry

lemma "{} = A - A"
nitpick [card = 1-100, expect = none]
by auto

lemma "g = Let (A \ B)"
nitpick [card = 1, expect = none]
nitpick [card = 12, expect = genuine]
oops

lemma "(let a_or_b = A \ B in a_or_b \ \ a_or_b)"
nitpick [expect = none]
by auto

lemma "A \ B"
nitpick [card = 100, expect = genuine]
oops

lemma "A = {b}"
nitpick [card = 100, expect = genuine]
oops

lemma "{a, b} = {b}"
nitpick [card = 50, expect = genuine]
oops

lemma "(a::'a\'a, a::'a\'a) \ R"
nitpick [card = 1, expect = genuine]
nitpick [card = 10, expect = genuine]
nitpick [card = 5, dont_box, expect = genuine]
oops

lemma "f (g::'a\'a) = x"
nitpick [card = 3, dont_box, expect = genuine]
nitpick [card = 8, expect = genuine]
oops

lemma "f (a, b) = x"
nitpick [card = 10, expect = genuine]
oops

lemma "f (a, a) = f (c, d)"
nitpick [card = 10, expect = genuine]
oops

lemma "(x::'a) = (\a. \b. \c. if c then a else b) x x True"
nitpick [card = 1-10, expect = none]
by auto

lemma "\F. F a b = G a b"
nitpick [card = 2, expect = none]
by auto

lemma "f = case_prod"
nitpick [card = 2, expect = genuine]
oops

lemma "(A::'a\'a, B::'a\'a) \ R \ (A, B) \ R"
nitpick [card = 15, expect = none]
by auto

lemma "(A, B) \ R \ (\C. (A, C) \ R \ (C, B) \ R) \
       A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
nitpick [card = 1-25, expect = none]
by auto

lemma "f = (\x::'a\'b. x)"
nitpick [card = 8, expect = genuine]
oops

subsection \<open>Quantifiers\<close>

lemma "x = y"
nitpick [card 'a = 1, expect = none]
nitpick [card 'a = 100, expect = genuine]
oops

lemma "\x. x = y"
nitpick [card 'a = 1, expect = none]
nitpick [card 'a = 100, expect = genuine]
oops

lemma "\x::'a \ bool. x = y"
nitpick [card 'a = 1, expect = genuine]
nitpick [card 'a = 100, expect = genuine]
oops

lemma "\x::'a \ bool. x = y"
nitpick [card 'a = 1-15, expect = none]
by auto

lemma "\x y::'a \ bool. x = y"
nitpick [card = 1-15, expect = none]
by auto

lemma "\x. \y. f x y = f x (g x)"
nitpick [card = 1-4, expect = none]
by auto

lemma "\u. \v. \w. \x. f u v w x = f u (g u) w (h u w)"
nitpick [card = 1-4, expect = none]
by auto

lemma "\u. \v. \w. \x. f u v w x = f u (g u w) w (h u)"
nitpick [card = 3, expect = genuine]
oops

lemma "\u. \v. \w. \x. \y. \z.
       f u v w x y z = f u (g u) w (h u w) y (k u w y)"
nitpick [card = 1-2, expect = none]
sorry

lemma "\u. \v. \w. \x. \y. \z.
       f u v w x y z = f u (g u) w (h u w y) y (k u w y)"
nitpick [card = 1-2, expect = genuine]
oops

lemma "\u. \v. \w. \x. \y. \z.
       f u v w x y z = f u (g u w) w (h u w) y (k u w y)"
nitpick [card = 1-2, expect = genuine]
oops

lemma "\u::'a \ 'b. \v::'c. \w::'d. \x::'e \ 'f.
       f u v w x = f u (g u) w (h u w)"
nitpick [card = 1-2, expect = none]
sorry

lemma "\u::'a \ 'b. \v::'c. \w::'d. \x::'e \ 'f.
       f u v w x = f u (g u w) w (h u)"
nitpick [card = 1-2, dont_box, expect = genuine]
oops

lemma "\u::'a \ 'b. \v::'c. \w::'d. \x::'e \ 'f.
       f u v w x = f u (g u) w (h u w)"
nitpick [card = 1-2, dont_box, expect = none]
sorry

lemma "\u::'a \ 'b. \v::'c. \w::'d. \x::'e \ 'f.
       f u v w x = f u (g u w) w (h u)"
nitpick [card = 1-2, dont_box, expect = genuine]
oops

lemma "\x. if (\y. x = y) then False else True"
nitpick [card = 1, expect = genuine]
nitpick [card = 2-5, expect = none]
oops

lemma "\x::'a\'b. if (\y. x = y) then False else True"
nitpick [card = 1, expect = genuine]
nitpick [card = 2, expect = none]
oops

lemma "\x. if (\y. x = y) then True else False"
nitpick [expect = none]
sorry

lemma "(\x::'a. \y. P x y) \ (\x::'a \ 'a. \y. P y x)"
nitpick [card 'a = 1, expect = genuine]
oops

lemma "\x. if x = y then (\y. y = x \ y \ x)
           else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
nitpick [expect = none]
by auto

lemma "\x. if x = y then (\y. y = x \ y \ x)
           else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))"
nitpick [expect = none]
by auto

lemma "let x = (\x. P x) in if x then x else \ x"
nitpick [expect = none]
by auto

lemma "let x = (\x::'a \ 'b. P x) in if x then x else \ x"
nitpick [expect = none]
by auto

subsection \<open>Schematic Variables\<close>

schematic_goal "x = ?x"
nitpick [expect = none]
by auto

schematic_goal "\x. x = ?x"
nitpick [expect = genuine]
oops

schematic_goal "\x. x = ?x"
nitpick [expect = none]
by auto

schematic_goal "\x::'a \ 'b. x = ?x"
nitpick [expect = none]
by auto

schematic_goal "\x. ?x = ?y"
nitpick [expect = none]
by auto

schematic_goal "\x. ?x = ?y"
nitpick [expect = none]
by auto

subsection \<open>Known Constants\<close>

lemma "x \ Pure.all \ False"
nitpick [card = 1, expect = genuine]
nitpick [card = 1, box "('a \ prop) \ prop", expect = genuine]
nitpick [card = 6, expect = genuine]
oops

lemma "\x. f x y = f x y"
nitpick [expect = none]
oops

lemma "\x. f x y = f y x"
nitpick [expect = genuine]
oops

lemma "Pure.all (\x. Trueprop (f x y = f x y)) \ Trueprop True"
nitpick [expect = none]
by auto

lemma "Pure.all (\x. Trueprop (f x y = f x y)) \ Trueprop False"
nitpick [expect = genuine]
oops

lemma "I = (\x. x) \ Pure.all P \ Pure.all (\x. P (I x))"
nitpick [expect = none]
by auto

lemma "x \ (\) \ False"
nitpick [card = 1, expect = genuine]
oops

lemma "P x \ P x"
nitpick [card = 1-10, expect = none]
by auto

lemma "P x \ Q x \ P x = Q x"
nitpick [card = 1-10, expect = none]
by auto

lemma "P x = Q x \ P x \ Q x"
nitpick [card = 1-10, expect = none]
by auto

lemma "x \ (\) \ False"
nitpick [expect = genuine]
oops

lemma "I \ (\x. x) \ ((\) x) \ (\y. ((\) x (I y)))"
nitpick [expect = none]
by auto

lemma "P x \ P x"
nitpick [card = 1-10, expect = none]
by auto

lemma "True \ True" "False \ True" "False \ False"
nitpick [expect = none]
by auto

lemma "True \ False"
nitpick [expect = genuine]
oops

lemma "x = Not"
nitpick [expect = genuine]
oops

lemma "I = (\x. x) \ Not = (\x. Not (I x))"
nitpick [expect = none]
by auto

lemma "x = True"
nitpick [expect = genuine]
oops

lemma "x = False"
nitpick [expect = genuine]
oops

lemma "x = undefined"
nitpick [expect = genuine]
oops

lemma "(False, ()) = undefined \ ((), False) = undefined"
nitpick [expect = genuine]
oops

lemma "undefined = undefined"
nitpick [expect = none]
by auto

lemma "f undefined = f undefined"
nitpick [expect = none]
by auto

lemma "f undefined = g undefined"
nitpick [card = 33, expect = genuine]
oops

lemma "\!x. x = undefined"
nitpick [card = 15, expect = none]
by auto

lemma "x = All \ False"
nitpick [card = 1, dont_box, expect = genuine]
oops

lemma "\x. f x y = f x y"
nitpick [expect = none]
oops

lemma "\x. f x y = f y x"
nitpick [expect = genuine]
oops

lemma "All (\x. f x y = f x y) = True"
nitpick [expect = none]
by auto

lemma "All (\x. f x y = f x y) = False"
nitpick [expect = genuine]
oops

lemma "x = Ex \ False"
nitpick [card = 1, dont_box, expect = genuine]
oops

lemma "\x. f x y = f x y"
nitpick [expect = none]
oops

lemma "\x. f x y = f y x"
nitpick [expect = none]
oops

lemma "Ex (\x. f x y = f x y) = True"
nitpick [expect = none]
by auto

lemma "Ex (\x. f x y = f y x) = True"
nitpick [expect = none]
by auto

lemma "Ex (\x. f x y = f x y) = False"
nitpick [expect = genuine]
oops

lemma "Ex (\x. f x y \ f x y) = False"
nitpick [expect = none]
by auto

lemma "I = (\x. x) \ Ex P = Ex (\x. P (I x))"
nitpick [expect = none]
by auto

lemma "x = y \ y = x"
nitpick [expect = none]
by auto

lemma "x = y \ f x = f y"
nitpick [expect = none]
by auto

lemma "x = y \ y = z \ x = z"
nitpick [expect = none]
by auto

lemma "I = (\x. x) \ (\) = (\x. (\) (I x))"
      "I = (\x. x) \ (\) = (\x y. x \ (I y))"
nitpick [expect = none]
by auto

lemma "(a \ b) = (\ (\ a \ \ b))"
nitpick [expect = none]
by auto

lemma "a \ b \ a" "a \ b \ b"
nitpick [expect = none]
by auto

lemma "(\) = (\x. (\) x)" "((\) ) = (\x y. x \ y)"
nitpick [expect = none]
by auto

lemma "((if a then b else c) = d) = ((a \ (b = d)) \ (\ a \ (c = d)))"
nitpick [expect = none]
by auto

lemma "(if a then b else c) = (THE d. (a \ (d = b)) \ (\ a \ (d = c)))"
nitpick [expect = none]
by auto

lemma "fst (x, y) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x, y) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "fst (x::'a\'b, y) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x::'a\'b, y) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "fst (x, y::'a\'b) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x, y::'a\'b) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "fst (x::'a\'b, y) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x::'a\'b, y) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "fst (x, y::'a\'b) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x, y::'a\'b) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "I = (\x. x) \ fst = (\x. fst (I x))"
nitpick [expect = none]
by auto

lemma "fst (x, y) = snd (y, x)"
nitpick [expect = none]
by auto

lemma "(x, x) \ Id"
nitpick [expect = none]
by auto

lemma "(x, y) \ Id \ x = y"
nitpick [expect = none]
by auto

lemma "I = (\x. x) \ Id = {x. I x \ Id}"
nitpick [expect = none]
by auto

lemma "{} = {x. False}"
nitpick [expect = none]
by (metis empty_def)

lemma "x \ {}"
nitpick [expect = genuine]
oops

lemma "{a, b} = {b}"
nitpick [expect = genuine]
oops

lemma "{a, b} \ {b}"
nitpick [expect = genuine]
oops

lemma "{a} = {b}"
nitpick [expect = genuine]
oops

lemma "{a} \ {b}"
nitpick [expect = genuine]
oops

lemma "{a, b, c} = {c, b, a}"
nitpick [expect = none]
by auto

lemma "UNIV = {x. True}"
nitpick [expect = none]
by (simp only: UNIV_def)

lemma "x \ UNIV \ True"
nitpick [expect = none]
by (simp only: UNIV_def mem_Collect_eq)

lemma "x \ UNIV"
nitpick [expect = genuine]
oops

lemma "I = (\x. x) \ (\) = (\x. ((\) (I x)))"
nitpick [expect = none]
apply (rule ext)
apply (rule ext)
by simp

lemma "insert = (\x y. insert x (y \ y))"
nitpick [expect = none]
by simp

lemma "I = (\x. x) \ trancl = (\x. trancl (I x))"
nitpick [card = 1-2, expect = none]
by auto

lemma "rtrancl = (\x. rtrancl x \ {(y, y)})"
nitpick [card = 1-3, expect = none]
apply (rule ext)
by auto

lemma "(x, x) \ rtrancl {(y, y)}"
nitpick [expect = none]
by auto

lemma "((x, x), (x, x)) \ rtrancl {}"
nitpick [card = 1-5, expect = none]
by auto

lemma "I = (\x. x) \ (\) = (\x. (\) (I x))"
nitpick [card = 1-5, expect = none]
by auto

lemma "a \ A \ a \ (A \ B)" "b \ B \ b \ (A \ B)"
nitpick [expect = none]
by auto

lemma "I = (\x. x) \ (\) = (\x. (\) (I x))"
nitpick [card = 1-5, expect = none]
by auto

lemma "a \ A \ a \ (A \ B)" "b \ B \ b \ (A \ B)"
nitpick [card = 1-5, expect = none]
by auto

lemma "x \ ((A::'a set) - B) \ x \ A \ x \ B"
nitpick [card = 1-5, expect = none]
by auto

lemma "I = (\x. x) \ (\) = (\x. (\) (I x))"
nitpick [card = 1-5, expect = none]
by auto

lemma "A \ B \ (\a \ A. a \ B) \ (\b \ B. b \ A)"
nitpick [card = 1-5, expect = none]
by auto

lemma "A \ B \ \a \ A. a \ B"
nitpick [card = 1-5, expect = none]
by auto

lemma "A \ B \ A \ B"
nitpick [card = 5, expect = genuine]
oops

lemma "A \ B \ A \ B"
nitpick [expect = none]
by auto

lemma "I = (\x::'a set. x) \ uminus = (\x. uminus (I x))"
nitpick [card = 1-7, expect = none]
by auto

lemma "A \ - A = UNIV"
nitpick [expect = none]
by auto

lemma "A \ - A = {}"
nitpick [expect = none]
by auto

lemma "A = -(A::'a set)"
nitpick [card 'a = 10, expect = genuine]
oops

lemma "finite A"
nitpick [expect = none]
oops

lemma "finite A \ finite B"
nitpick [expect = none]
oops

lemma "All finite"
nitpick [expect = none]
oops

subsection \<open>The and Eps\<close>

lemma "x = The"
nitpick [card = 5, expect = genuine]
oops

lemma "\x. x = The"
nitpick [card = 1-3]
by auto

lemma "P x \ (\y. P y \ y = x) \ The P = x"
nitpick [expect = none]
by auto

lemma "P x \ P y \ x \ y \ The P = z"
nitpick [expect = genuine]
oops

lemma "P x \ P y \ x \ y \ The P = x \ The P = y"
nitpick [card = 2, expect = none]
nitpick [card = 3-5, expect = genuine]
oops

lemma "P x \ P (The P)"
nitpick [card = 1-2, expect = none]
nitpick [card = 8, expect = genuine]
oops

lemma "(\x. \ P x) \ The P = y"
nitpick [expect = genuine]
oops

lemma "I = (\x. x) \ The = (\x. The (I x))"
nitpick [card = 1-5, expect = none]
by auto

lemma "x = Eps"
nitpick [card = 5, expect = genuine]
oops

lemma "\x. x = Eps"
nitpick [card = 1-3, expect = none]
by auto

lemma "P x \ (\y. P y \ y = x) \ Eps P = x"
nitpick [expect = none]
by auto

lemma "P x \ P y \ x \ y \ Eps P = z"
nitpick [expect = genuine]
apply auto
oops

lemma "P x \ P (Eps P)"
nitpick [card = 1-8, expect = none]
by (metis exE_some)

lemma "\x. \ P x \ Eps P = y"
nitpick [expect = genuine]
oops

lemma "P (Eps P)"
nitpick [expect = genuine]
oops

lemma "Eps (\x. x \ P) \ (P::nat set)"
nitpick [expect = genuine]
oops

lemma "\ P (Eps P)"
nitpick [expect = genuine]
oops

lemma "\ (P :: nat \ bool) (Eps P)"
nitpick [expect = genuine]
oops

lemma "P \ bot \ P (Eps P)"
nitpick [expect = none]
sorry

lemma "(P :: nat \ bool) \ bot \ P (Eps P)"
nitpick [expect = none]
sorry

lemma "P (The P)"
nitpick [expect = genuine]
oops

lemma "(P :: nat \ bool) (The P)"
nitpick [expect = genuine]
oops

lemma "\ P (The P)"
nitpick [expect = genuine]
oops

lemma "\ (P :: nat \ bool) (The P)"
nitpick [expect = genuine]
oops

lemma "The P \ x"
nitpick [expect = genuine]
oops

lemma "The P \ (x::nat)"
nitpick [expect = genuine]
oops

lemma "P x \ P (The P)"
nitpick [expect = genuine]
oops

lemma "P (x::nat) \ P (The P)"
nitpick [expect = genuine]
oops

lemma "P = {x} \ (THE x. x \ P) \ P"
nitpick [expect = none]
oops

lemma "P = {x::nat} \ (THE x. x \ P) \ P"
nitpick [expect = none]
oops

consts Q :: 'a

lemma "Q (Eps Q)"
nitpick [expect = genuine]
oops

lemma "(Q :: nat \ bool) (Eps Q)"
nitpick [expect = none] (* unfortunate *)
oops

lemma "\ (Q :: nat \ bool) (Eps Q)"
nitpick [expect = genuine]
oops

lemma "\ (Q :: nat \ bool) (Eps Q)"
nitpick [expect = genuine]
oops

lemma "(Q::'a \ bool) \ bot \ (Q::'a \ bool) (Eps Q)"
nitpick [expect = none]
sorry

lemma "(Q::nat \ bool) \ bot \ (Q::nat \ bool) (Eps Q)"
nitpick [expect = none]
sorry

lemma "Q (The Q)"
nitpick [expect = genuine]
oops

lemma "(Q::nat \ bool) (The Q)"
nitpick [expect = genuine]
oops

lemma "\ Q (The Q)"
nitpick [expect = genuine]
oops

lemma "\ (Q::nat \ bool) (The Q)"
nitpick [expect = genuine]
oops

lemma "The Q \ x"
nitpick [expect = genuine]
oops

lemma "The Q \ (x::nat)"
nitpick [expect = genuine]
oops

lemma "Q x \ Q (The Q)"
nitpick [expect = genuine]
oops

lemma "Q (x::nat) \ Q (The Q)"
nitpick [expect = genuine]
oops

lemma "Q = (\x::'a. x = a) \ (Q::'a \ bool) (The Q)"
nitpick [expect = none]
sorry

lemma "Q = (\x::nat. x = a) \ (Q::nat \ bool) (The Q)"
nitpick [expect = none]
sorry

nitpick_params [max_potential = 1]

lemma "(THE j. j > Suc 2 \ j \ 3) \ 0"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = potential] (* unfortunate *)
oops

lemma "(THE j. j > Suc 2 \ j \ 4) = x \ x \ 0"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = none]
sorry

lemma "(THE j. j > Suc 2 \ j \ 4) = x \ x = 4"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = none]
sorry

lemma "(THE j. j > Suc 2 \ j \ 5) = x \ x = 4"
nitpick [card nat = 6, expect = genuine]
oops

lemma "(THE j. j > Suc 2 \ j \ 5) = x \ x = 4 \ x = 5"
nitpick [card nat = 6, expect = genuine]
oops

lemma "(SOME j. j > Suc 2 \ j \ 3) \ 0"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = genuine]
oops

lemma "(SOME j. j > Suc 2 \ j \ 4) = x \ x \ 0"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = none]
oops

lemma "(SOME j. j > Suc 2 \ j \ 4) = x \ x = 4"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = none]
sorry

lemma "(SOME j. j > Suc 2 \ j \ 5) = x \ x = 4"
nitpick [card nat = 6, expect = genuine]
oops

lemma "(SOME j. j > Suc 2 \ j \ 5) = x \ x = 4 \ x = 5"
nitpick [card nat = 6, expect = none]
sorry

nitpick_params [max_potential = 0]

subsection \<open>Destructors and Recursors\<close>

lemma "(x::'a) = (case True of True \ x | False \ x)"
nitpick [card = 2, expect = none]
by auto

lemma "x = (case (x, y) of (x', y') \ x')"
nitpick [expect = none]
sorry

end

¤ Dauer der Verarbeitung: 0.29 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.