(* hiding set *) translations "xs" <= "CONST set xs"
(* hiding numeric conversions - embeddings only *) translations "n" <= "CONST of_nat n" "n" <= "CONST int n" "n" <= "CONST real n" "n" <= "CONST real_of_nat n" "n" <= "CONST real_of_int n" "n" <= "CONST of_real n" "n" <= "CONST complex_of_real n"
(* append *) syntax (latex output) "_appendL" :: "'a list \ 'a list \ 'a list" (infixl \\<^latex>\\isacharat\\ 65) translations "_appendL xs ys" <= "xs @ ys" "_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
(* deprecated, use thm with style instead, will be removed *) (* aligning equations *) notation (tab output) "HOL.eq" (\<open>(_) \<^latex>\<open>}\putisatab\isa{\ \<close>=\<^latex>\<open>}\putisatab\isa{\<close> (_)\<close> [50,49] 50) and "Pure.eq" (\<open>(_) \<^latex>\<open>}\putisatab\isa{\ \<close>\<equiv>\<^latex>\<open>}\putisatab\isa{\<close> (_)\<close>)
(* Let *) translations "_bind (p, CONST DUMMY) e" <= "_bind p (CONST fst e)" "_bind (CONST DUMMY, p) e" <= "_bind p (CONST snd e)"
"_tuple_args x (_tuple_args y z)" == "_tuple_args x (_tuple_arg (_tuple y z))"
"_bind (CONST Some p) e" <= "_bind p (CONST the e)" "_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)" "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
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.
