# HG changeset patch # User nipkow # Date 1106738416 -3600 # Node ID f0138af74b387a531aacd88604722f6791b1dfa8 # Parent 8447132f4ff5b6c65a7a2d82592129bbed60c718 moved to HOL/Library diff -r 8447132f4ff5 -r f0138af74b38 doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy --- a/doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy Wed Jan 26 12:20:07 2005 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,83 +0,0 @@ -(*<*) -theory LaTeXsugar -imports Main -begin - -(* LOGIC *) -syntax (latex output) - If :: "[bool, 'a, 'a] => 'a" - ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10) - - "_Let" :: "[letbinds, 'a] => 'a" - ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10) - - "_case_syntax":: "['a, cases_syn] => 'b" - ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10) - -(* SETS *) - -(* empty set *) -syntax (latex output) - "_emptyset" :: "'a set" ("\") -translations - "_emptyset" <= "{}" - -(* insert *) -translations - "{x} \ A" <= "insert x A" - "{x,y} \ A" <= "{x} \ ({y} \ A)" - -(* set comprehension *) -syntax (latex output) - "_Collect" :: "pttrn => bool => 'a set" ("(1{_ | _})") -translations - "_Collect p P" <= "{p. 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" ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000) - -(* DUMMY *) -consts DUMMY :: 'a ("\<^raw:\_>") - -(* THEOREMS *) -syntax (Rule output) - "==>" :: "prop \ prop \ prop" - ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") - - "_bigimpl" :: "asms \ prop \ prop" - ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") - - "_asms" :: "prop \ asms \ asms" - ("\<^raw:\mbox{>_\<^raw:}\\>/ _") - - "_asm" :: "prop \ asms" ("\<^raw:\mbox{>_\<^raw:}>") - -syntax (IfThen output) - "==>" :: "prop \ prop \ prop" - ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") - "_bigimpl" :: "asms \ prop \ prop" - ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") - "_asms" :: "prop \ asms \ asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _") - "_asm" :: "prop \ asms" ("\<^raw:\mbox{>_\<^raw:}>") - -syntax (IfThenNoBox output) - "==>" :: "prop \ prop \ prop" - ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") - "_bigimpl" :: "asms \ prop \ prop" - ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") - "_asms" :: "prop \ asms \ asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _") - "_asm" :: "prop \ asms" ("_") - -end -(*>*) \ No newline at end of file diff -r 8447132f4ff5 -r f0138af74b38 doc-src/LaTeXsugar/Sugar/OptionalSugar.thy --- a/doc-src/LaTeXsugar/Sugar/OptionalSugar.thy Wed Jan 26 12:20:07 2005 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,31 +0,0 @@ -theory OptionalSugar -imports LaTeXsugar -begin - -(* append *) -syntax (latex output) - "appendL" :: "'a list \ 'a list \ 'a list" (infixl "\<^raw:\isacharat>" 65) -translations - "appendL xs ys" <= "xs @ ys" - "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)" - - -(* aligning equations *) -syntax (tab output) - "op =" :: "'a \ 'a \ 'a" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) - "==" :: "prop \ prop \ prop" ("(_) \<^raw:}\putisatab\isa{\ >\\<^raw:}\putisatab\isa{> (_)") - -(* Let *) -translations - "_bind (p,DUMMY) e" <= "_bind p (fst e)" - "_bind (DUMMY,p) e" <= "_bind p (snd e)" - - "_tuple_args x (_tuple_args y z)" == - "_tuple_args x (_tuple_arg (_tuple y z))" - - "_bind (Some p) e" <= "_bind p (the e)" - "_bind (p#DUMMY) e" <= "_bind p (hd e)" - "_bind (DUMMY#p) e" <= "_bind p (tl e)" - - -end \ No newline at end of file