(* Title: HOL/Library/LaTeXsugar.thy ID: $Id: LaTeXsugar.thy,v 1.4 2005/05/30 06:22:54 nipkow Exp $ Author: Gerwin Klain, Tobias Nipkow, Norbert Schirmer Copyright 2005 NICTA and TUM *) (*<*) theory LaTeXsugar imports Main begin (* LOGIC *) syntax (latex output) If :: "[bool, 'a, 'a] => 'a" ("(\textsf{if} (_)/ \textsf{then} (_)/ \textsf{else} (_))" 10) "_Let" :: "[letbinds, 'a] => 'a" ("(\textsf{let} (_)/ \textsf{in} (_))" 10) "_case_syntax":: "['a, cases_syn] => 'b" ("(\textsf{case} _ \textsf{of}/ _)" 10) (* should become standard syntax once x-symbols supports it *) syntax (latex) nexists :: "('a => bool) => bool" (binder "\<nexists>" 10) translations "\<nexists>x. P" <= "¬(∃x. P)" (* SETS *) (* empty set *) syntax (latex output) "_emptyset" :: "'a set" ("∅") translations "_emptyset" <= "{}" (* insert *) translations "{x} ∪ A" <= "insert x A" "{x,y}" <= "{x} ∪ {y}" "{x,y} ∪ A" <= "{x} ∪ ({y} ∪ A)" "{x}" <= "{x} ∪ _emptyset" (* set comprehension *) syntax (latex output) "_Collect" :: "pttrn => bool => 'a set" ("(1{_ | _})") translations "_Collect p P" <= "{p. P}" "_Collect p P" <= "{p|xs. P}" (* LISTS *) (* Cons *) syntax (latex) Cons :: "'a => 'a list => 'a list" ("_·/_" [66,65] 65) (* length *) syntax (latex output) length :: "'a list => nat" ("|_|") (* nth *) syntax (latex output) nth :: "'a list => nat => 'a" ("_\ensuremath{_{[\mathit{_}]}}" [1000,0] 1000) (* DUMMY *) consts DUMMY :: 'a ("\_") (* THEOREMS *) syntax (Rule output) "==>" :: "prop => prop => prop" ("\mbox{}\inferrule{\mbox{_}}{\mbox{_}}") "_bigimpl" :: "asms => prop => prop" ("\mbox{}\inferrule{_}{\mbox{_}}") "_asms" :: "prop => asms => asms" ("\mbox{_}\\/ _") "_asm" :: "prop => asms" ("\mbox{_}") syntax (IfThen output) "==>" :: "prop => prop => prop" ("{\rmfamily\upshape\normalsize{}If\,} _/ {\rmfamily\upshape\normalsize \,then\,}/ _.") "_bigimpl" :: "asms => prop => prop" ("{\rmfamily\upshape\normalsize{}If\,} _ /{\rmfamily\upshape\normalsize \,then\,}/ _.") "_asms" :: "prop => asms => asms" ("\mbox{_} /{\rmfamily\upshape\normalsize \,and\,}/ _") "_asm" :: "prop => asms" ("\mbox{_}") syntax (IfThenNoBox output) "==>" :: "prop => prop => prop" ("{\rmfamily\upshape\normalsize{}If\,} _/ {\rmfamily\upshape\normalsize \,then\,}/ _.") "_bigimpl" :: "asms => prop => prop" ("{\rmfamily\upshape\normalsize{}If\,} _ /{\rmfamily\upshape\normalsize \,then\,}/ _.") "_asms" :: "prop => asms => asms" ("_ /{\rmfamily\upshape\normalsize \,and\,}/ _") "_asm" :: "prop => asms" ("_") end (*>*)