src/HOL/Library/LaTeXsugar.thy
changeset 15469 f5d22f504ab9
child 15476 b8cb20cc0c0b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Wed Jan 26 13:50:59 2005 +0100
     1.3 @@ -0,0 +1,89 @@
     1.4 +(*  Title:      HOL/Library/LaTeXsugar.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Gerwin Klain, Tobias Nipkow, Norbert Schirmer
     1.7 +    Copyright   2005 NICTA and TUM
     1.8 +*)
     1.9 +
    1.10 +(*<*)
    1.11 +theory LaTeXsugar
    1.12 +imports Main
    1.13 +begin
    1.14 +
    1.15 +(* LOGIC *)
    1.16 +syntax (latex output)
    1.17 +  If            :: "[bool, 'a, 'a] => 'a"
    1.18 +  ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
    1.19 +
    1.20 +  "_Let"        :: "[letbinds, 'a] => 'a"
    1.21 +  ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10)
    1.22 +
    1.23 +  "_case_syntax":: "['a, cases_syn] => 'b"
    1.24 +  ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
    1.25 +
    1.26 +(* SETS *)
    1.27 +
    1.28 +(* empty set *)
    1.29 +syntax (latex output)
    1.30 +  "_emptyset" :: "'a set"              ("\<emptyset>")
    1.31 +translations
    1.32 +  "_emptyset"      <= "{}"
    1.33 +
    1.34 +(* insert *)
    1.35 +translations 
    1.36 +  "{x} \<union> A" <= "insert x A"
    1.37 +  "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
    1.38 +
    1.39 +(* set comprehension *)
    1.40 +syntax (latex output)
    1.41 +  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
    1.42 +translations
    1.43 +  "_Collect p P"      <= "{p. P}"
    1.44 +
    1.45 +(* LISTS *)
    1.46 +
    1.47 +(* Cons *)
    1.48 +syntax (latex)
    1.49 +  Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_\<cdot>/_" [66,65] 65)
    1.50 +
    1.51 +(* length *)
    1.52 +syntax (latex output)
    1.53 +  length :: "'a list \<Rightarrow> nat" ("|_|")
    1.54 +
    1.55 +(* nth *)
    1.56 +syntax (latex output)
    1.57 +  nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
    1.58 +
    1.59 +(* DUMMY *)
    1.60 +consts DUMMY :: 'a ("\<^raw:\_>")
    1.61 +
    1.62 +(* THEOREMS *)
    1.63 +syntax (Rule output)
    1.64 +  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    1.65 +  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    1.66 +
    1.67 +  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.68 +  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    1.69 +
    1.70 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
    1.71 +  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
    1.72 +
    1.73 +  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    1.74 +
    1.75 +syntax (IfThen output)
    1.76 +  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    1.77 +  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    1.78 +  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.79 +  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    1.80 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
    1.81 +  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    1.82 +
    1.83 +syntax (IfThenNoBox output)
    1.84 +  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    1.85 +  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    1.86 +  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.87 +  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    1.88 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
    1.89 +  "_asm" :: "prop \<Rightarrow> asms" ("_")
    1.90 +
    1.91 +end
    1.92 +(*>*)
    1.93 \ No newline at end of file