text‹In this theory we mainly provide some Isabelle/ML infrastructure
that is used by several generators. It consists of a uniform interface
to access all the theorems, terms, etc.\ from the BNF package, and
some auxiliary functions which provide recursors on datatypes, common tactics, etc.›
lemma in_set_simps: "x ∈ set (y # z # ys) = (x = y ∨ x ∈ set (z # ys))" "x ∈ set ([y]) = (x = y)" "x ∈ set [] = False" "Ball (set []) P = True" "Ball (set [x]) P = P x" "Ball (set (x # y # zs)) P = (P x ∧ Ball (set (y # zs)) P)" by auto
lemma conj_weak_cong: "a = b ==> c = d ==> (a ∧ c) = (b ∧ d)"by auto
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 und die Messung sind noch experimentell.
